1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
34
(* Errors raised by the refiner *)
35
| BadType of constr * constr * constr
36
| UnresolvedBindings of name list
37
| CannotApply of constr * constr
38
| NotWellTyped of constr
39
| NonLinearProof of constr
40
| MetaInType of constr
42
(* Errors raised by the tactics *)
44
| DoesNotOccurIn of constr * identifier
46
exception RefinerError of refiner_error
50
let rec catchable_exception = function
51
| Stdpp.Exc_located(_,e) -> catchable_exception e
52
| LtacLocated(_,e) -> catchable_exception e
53
| Util.UserError _ | TypeError _
54
| RefinerError _ | Indrec.RecursionSchemeError _
55
| Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
56
(* unification errors *)
57
| PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
58
|NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
59
|CannotFindWellTypedAbstraction _
60
|UnsolvableImplicit _)) -> true
61
| Typeclasses_errors.TypeClassError
62
(_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
65
let error_no_such_hypothesis id =
66
error ("No such hypothesis: " ^ string_of_id id ^ ".")
68
(* Tells if the refiner should check that the submitted rules do not
69
produce invalid subgoals *)
71
let with_check = Flags.with_option check
73
(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
74
returns [tail::(f head (id,_,_) (rev tail))] *)
75
let apply_to_hyp sign id f =
76
try apply_to_hyp sign id f
78
if !check then error "No such assumption."
81
let apply_to_hyp_and_dependent_on sign id f g =
82
try apply_to_hyp_and_dependent_on sign id f g
84
if !check then error "No such assumption."
87
let check_typability env sigma c =
88
if !check then let _ = type_of env sigma c in ()
90
(************************************************************************)
91
(************************************************************************)
92
(* Implementation of the structural rules (moving and deleting
95
(* The Clear tactic: it scans the context for hypotheses to be removed
96
(instead of iterating on the list of identifier to be removed, which
97
forces the user to give them in order). *)
99
let clear_hyps sigma ids sign cl =
100
let evdref = ref (Evd.create_goal_evar_defs sigma) in
101
let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
102
(hyps,concl,evars_of !evdref)
104
(* The ClearBody tactic *)
106
let recheck_typability (what,id) env sigma t =
107
try check_typability env sigma t
109
let s = match what with
110
| None -> "the conclusion"
111
| Some id -> "hypothesis "^(string_of_id id) in
113
("The correctness of "^s^" relies on the body of "^(string_of_id id))
115
let remove_hyp_body env sigma id =
117
apply_to_hyp_and_dependent_on (named_context_val env) id
120
| None -> error ((string_of_id id)^" is not a local definition.")
121
| Some c ->(id,None,t))
122
(fun (id',c,t as d) sign ->
125
let env = reset_with_named_context sign env in
127
| None -> recheck_typability (Some id',id) env sigma t
129
let b' = mkCast (b,DEFAULTcast, t) in
130
recheck_typability (Some id',id) env sigma b'
133
reset_with_named_context sign env
135
(* Reordering of the context *)
137
(* faire le minimum d'echanges pour que l'ordre donne soit un *)
138
(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
139
(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
140
(* reculees par rapport aux autres (faire le contraire!) *)
142
let mt_q = (Idmap.empty,[])
143
let push_val y = function
145
| (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
146
let push_item x v (m,l) =
147
(Idmap.add x v m, (x,Idset.empty)::l)
148
let mem_q x (m,_) = Idmap.mem x m
149
let rec find_q x (m,q) =
150
let v = Idmap.find x m in
151
let m' = Idmap.remove x m in
152
let rec find accs acc = function
153
[] -> raise Not_found
155
if x=x' then ((v,Idset.union accs l),(m',List.rev acc))
157
| (x',l as i)::((x'',l'')::q as itl) ->
159
((v,Idset.union accs l),
160
(m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
161
else find (Idset.union l accs) (i::acc) itl in
162
find Idset.empty [] q
164
let occur_vars_in_decl env hyps d =
165
if Idset.is_empty hyps then false else
166
let ohyps = global_vars_set_of_decl env d in
167
Idset.exists (fun h -> Idset.mem h ohyps) hyps
169
let reorder_context env sign ord =
170
let ords = List.fold_right Idset.add ord Idset.empty in
171
if List.length ord <> Idset.cardinal ords then
172
error "Order list has duplicates";
173
let rec step ord expected ctxt_head moved_hyps ctxt_tail =
175
| [] -> List.rev ctxt_tail @ ctxt_head
176
| top::ord' when mem_q top moved_hyps ->
177
let ((d,h),mh) = find_q top moved_hyps in
178
if occur_vars_in_decl env h d then
179
errorlabstrm "reorder_context"
180
(str "Cannot move declaration " ++ pr_id top ++ spc() ++
182
prlist_with_sep pr_spc pr_id
183
(Idset.elements (Idset.inter h
184
(global_vars_set_of_decl env d))));
185
step ord' expected ctxt_head mh (d::ctxt_tail)
187
(match ctxt_head with
188
| [] -> error_no_such_hypothesis (List.hd ord)
189
| (x,_,_ as d) :: ctxt ->
190
if Idset.mem x expected then
191
step ord (Idset.remove x expected)
192
ctxt (push_item x d moved_hyps) ctxt_tail
195
ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
196
step ord ords sign mt_q []
198
let reorder_val_context env sign ord =
199
val_of_named_context (reorder_context env (named_context_of_val sign) ord)
204
let check_decl_position env sign (x,_,_ as d) =
205
let needed = global_vars_set_of_decl env d in
206
let deps = dependency_closure env (named_context_of_val sign) needed in
207
if List.mem x deps then
208
error ("Cannot create self-referring hypothesis "^string_of_id x);
211
(* Auxiliary functions for primitive MOVE tactic
213
* [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
214
* hyp [hfrom] at location [hto] which belongs to the hyps on the
215
* left side [left] of the full signature if [toleft=true] or to the hyps
216
* on the right side [right] if [toleft=false].
217
* If [with_dep] then dependent hypotheses are moved accordingly. *)
219
let rec get_hyp_after h = function
220
| [] -> error_no_such_hypothesis h
221
| (hyp,_,_) :: right ->
223
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false
225
get_hyp_after h right
227
let split_sign hfrom hto l =
228
let rec splitrec left toleft = function
229
| [] -> error_no_such_hypothesis hfrom
230
| (hyp,c,typ) as d :: right ->
232
(left,right,d, toleft or hto = MoveToEnd true)
235
(toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
240
let hyp_of_move_location = function
242
| MoveBefore id -> id
245
let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
246
let env = Global.env() in
247
let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
249
then occur_var_in_decl env hyp2 d
250
else occur_var_in_decl env hyp d2
252
let rec moverec first middle = function
254
if match hto with MoveToEnd _ -> false | _ -> true then
255
error_no_such_hypothesis (hyp_of_move_location hto);
256
List.rev first @ List.rev middle
257
| (hyp,_,_) :: _ as right when hto = MoveBefore hyp ->
258
List.rev first @ List.rev middle @ right
259
| (hyp,_,_) as d :: right ->
260
let (first',middle') =
261
if List.exists (test_dep d) middle then
262
if with_dep & hto <> MoveAfter hyp then
265
errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++
266
pr_move_location pr_id hto ++
267
str (if toleft then ": it occurs in " else ": it depends on ")
268
++ pr_id hyp ++ str ".")
272
if hto = MoveAfter hyp then
273
List.rev first' @ List.rev middle' @ right
275
moverec first' middle' right
279
List.fold_right push_named_context_val right empty_named_context_val in
280
List.fold_left (fun sign d -> push_named_context_val d sign)
281
right (moverec [] [declfrom] left)
284
List.fold_right push_named_context_val
285
(moverec [] [declfrom] right) empty_named_context_val in
286
List.fold_left (fun sign d -> push_named_context_val d sign)
289
let rename_hyp id1 id2 sign =
290
apply_to_hyp_and_dependent_on sign id1
291
(fun (_,b,t) _ -> (id2,b,t))
292
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
294
(************************************************************************)
295
(************************************************************************)
296
(* Implementation of the logical rules *)
298
(* Will only be used on terms given to the Refine rule which have meta
299
variables only in Application and Case *)
301
let error_unsupported_deep_meta c =
302
errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
303
strbrk "form contains metavariables deep inside the term is not " ++
304
strbrk "supported; try \"refine\" instead.")
306
let collect_meta_variables c =
307
let rec collrec deep acc c = match kind_of_term c with
308
| Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
309
| Cast(c,_,_) -> collrec deep acc c
310
| (App _| Case _) -> fold_constr (collrec deep) acc c
311
| _ -> fold_constr (collrec true) acc c
313
List.rev (collrec false [] c)
315
let check_meta_variables c =
316
if not (list_distinct (collect_meta_variables c)) then
317
raise (RefinerError (NonLinearProof c))
319
let check_conv_leq_goal env sigma arg ty conclty =
320
if !check & not (is_conv_leq env sigma ty conclty) then
321
raise (RefinerError (BadType (arg,ty,conclty)))
323
let goal_type_of env sigma c =
324
(if !check then type_of else Retyping.get_type_of) env sigma c
326
let rec mk_refgoals sigma goal goalacc conclty trm =
327
let env = evar_env goal in
328
let hyps = goal.evar_hyps in
329
let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
331
if not (occur_meta trm) then
332
let t'ty = (unsafe_machine env sigma trm).uj_type in
333
let _ = conv_leq_goal env sigma trm t'ty conclty in
337
match kind_of_term trm with
339
let conclty = nf_betaiota sigma conclty in
340
if !check && occur_meta conclty then
341
raise (RefinerError (MetaInType conclty));
342
(mk_goal hyps conclty)::goalacc, conclty
345
check_typability env sigma ty;
346
check_conv_leq_goal env sigma trm ty conclty;
347
mk_refgoals sigma goal goalacc ty t
351
match kind_of_term f with
353
when (isInd f or has_polymorphic_type (destConst f)) ->
354
(* Sort-polymorphism of definition and inductive types *)
356
type_of_global_reference_knowing_conclusion env sigma f conclty
358
mk_hdgoals sigma goal goalacc f
360
let (acc'',conclty') =
361
mk_arggoals sigma goal acc' hdty (Array.to_list l) in
362
check_conv_leq_goal env sigma trm conclty' conclty;
366
let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
367
check_conv_leq_goal env sigma trm conclty' conclty;
370
(fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
376
if occur_meta trm then
377
anomaly "refiner called with a meta in non app/case subterm";
379
let t'ty = goal_type_of env sigma trm in
380
check_conv_leq_goal env sigma trm t'ty conclty;
383
(* Same as mkREFGOALS but without knowing te type of the term. Therefore,
384
* Metas should be casted. *)
386
and mk_hdgoals sigma goal goalacc trm =
387
let env = evar_env goal in
388
let hyps = goal.evar_hyps in
389
let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
390
match kind_of_term trm with
391
| Cast (c,_, ty) when isMeta c ->
392
check_typability env sigma ty;
393
(mk_goal hyps (nf_betaiota sigma ty))::goalacc,ty
396
check_typability env sigma ty;
397
mk_refgoals sigma goal goalacc ty t
401
if isInd f or isConst f
402
& not (array_exists occur_meta l) (* we could be finer *)
404
(goalacc,type_of_global_reference_knowing_parameters env sigma f l)
405
else mk_hdgoals sigma goal goalacc f
407
mk_arggoals sigma goal acc' hdty (Array.to_list l)
410
let (acc',lbrty,conclty') = mk_casegoals sigma goal goalacc p c in
413
(fun lacc ty fi -> fst (mk_refgoals sigma goal lacc ty fi))
419
if !check && occur_meta trm then
420
anomaly "refined called with a dependent meta";
421
goalacc, goal_type_of env sigma trm
423
and mk_arggoals sigma goal goalacc funty = function
424
| [] -> goalacc,funty
425
| harg::tlargs as allargs ->
426
let t = whd_betadeltaiota (evar_env goal) sigma funty in
427
match kind_of_term t with
429
let (acc',hargty) = mk_refgoals sigma goal goalacc c1 harg in
430
mk_arggoals sigma goal acc' (subst1 harg b) tlargs
431
| LetIn (_,c1,_,b) ->
432
mk_arggoals sigma goal goalacc (subst1 c1 b) allargs
433
| _ -> raise (RefinerError (CannotApply (t,harg)))
435
and mk_casegoals sigma goal goalacc p c =
436
let env = evar_env goal in
437
let (acc',ct) = mk_hdgoals sigma goal goalacc c in
438
let (acc'',pt) = mk_hdgoals sigma goal acc' p in
439
let pj = {uj_val=p; uj_type=pt} in
441
try find_mrectype env sigma ct
442
with Not_found -> anomaly "mk_casegoals" in
443
let (lbrty,conclty) =
444
type_case_branches_with_names env indspec pj c in
445
(acc'',lbrty,conclty)
448
let convert_hyp sign sigma (id,b,bt as d) =
449
let env = Global.env() in
450
let reorder = ref [] in
454
let env = Global.env_of_context sign in
455
if !check && not (is_conv env sigma bt ct) then
456
error ("Incorrect change of the type of "^(string_of_id id)^".");
457
if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
458
error ("Incorrect change of the body of "^(string_of_id id)^".");
459
if !check then reorder := check_decl_position env sign d;
461
reorder_val_context env sign' !reorder
463
(* Normalizing evars in a goal. Called by tactic Local_constraints
464
(i.e. when the sigma of the proof tree changes). Detect if the
466
let norm_goal sigma gl =
467
let red_fun = Evarutil.nf_evar sigma in
468
let ncl = red_fun gl.evar_concl in
472
evar_hyps = map_named_val red_fun gl.evar_hyps } in
473
if Evd.eq_evar_info ngl gl then None else Some ngl
477
(************************************************************************)
478
(************************************************************************)
479
(* Primitive tactics are handled here *)
481
let prim_refiner r sigma goal =
482
let env = evar_env goal in
483
let sign = goal.evar_hyps in
484
let cl = goal.evar_concl in
485
let mk_goal hyps concl = mk_goal hyps concl goal.evar_extra in
489
if !check && mem_named_context id (named_context_of_val sign) then
490
error "New variable is already declared";
491
(match kind_of_term (strip_outer_cast cl) with
493
let sg = mk_goal (push_named_context_val (id,None,c1) sign)
494
(subst1 (mkVar id) b) in
496
| LetIn (_,c1,t1,b) ->
498
mk_goal (push_named_context_val (id,Some c1,t1) sign)
499
(subst1 (mkVar id) b) in
502
raise (RefinerError IntroNeedsProduct))
504
| Cut (b,replace,id,t) ->
505
let sg1 = mk_goal sign (nf_betaiota sigma t) in
508
let nexthyp = get_hyp_after id (named_context_of_val sign) in
509
let sign,cl,sigma = clear_hyps sigma [id] sign cl in
510
move_hyp true false ([],(id,None,t),named_context_of_val sign)
514
(if !check && mem_named_context id (named_context_of_val sign) then
515
error "New variable is already declared";
516
push_named_context_val (id,None,t) sign,cl,sigma) in
517
let sg2 = mk_goal sign cl in
518
if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
520
| FixRule (f,n,rest,j) ->
521
let rec check_ind env k cl =
522
match kind_of_term (strip_outer_cast cl) with
526
fst (find_inductive env sigma c1)
528
error "Cannot do a fixpoint on a non inductive type."
530
check_ind (push_rel (na,None,c1) env) (k-1) b
531
| _ -> error "Not enough products."
533
let (sp,_) = check_ind env n cl in
534
let firsts,lasts = list_chop j rest in
535
let all = firsts@(f,n,cl)::lasts in
536
let rec mk_sign sign = function
538
let (sp',_) = check_ind env n ar in
540
error ("Fixpoints should be on the same " ^
541
"mutual inductive declaration.");
542
if !check && mem_named_context f (named_context_of_val sign) then
544
("Name "^string_of_id f^" already used in the environment");
545
mk_sign (push_named_context_val (f,None,ar) sign) oth
547
List.map (fun (_,_,c) -> mk_goal sign c) all
549
(mk_sign sign all, sigma)
551
| Cofix (f,others,j) ->
552
let rec check_is_coind env cl =
553
let b = whd_betadeltaiota env sigma cl in
554
match kind_of_term b with
555
| Prod (na,c1,b) -> check_is_coind (push_rel (na,None,c1) env) b
558
let _ = find_coinductive env sigma b in ()
560
error ("All methods must construct elements " ^
561
"in coinductive types.")
563
let firsts,lasts = list_chop j others in
564
let all = firsts@(f,cl)::lasts in
565
List.iter (fun (_,c) -> check_is_coind env c) all;
566
let rec mk_sign sign = function
569
(let _ = lookup_named_val f sign in
570
error "Name already used in the environment.")
573
mk_sign (push_named_context_val (f,None,ar) sign) oth)
574
| [] -> List.map (fun (_,c) -> mk_goal sign c) all
576
(mk_sign sign all, sigma)
579
check_meta_variables c;
580
let (sgl,cl') = mk_refgoals sigma goal [] cl c in
581
let sgl = List.rev sgl in
584
(* Conversion rules *)
585
| Convert_concl (cl',_) ->
586
check_typability env sigma cl';
587
if (not !check) || is_conv_leq env sigma cl' cl then
588
let sg = mk_goal sign cl' in
591
error "convert-concl rule passed non-converting term"
593
| Convert_hyp (id,copt,ty) ->
594
([mk_goal (convert_hyp sign sigma (id,copt,ty)) cl], sigma)
596
(* And now the structural rules *)
598
let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
599
([mk_goal hyps concl], nsigma)
602
let clear_aux env id =
603
let env' = remove_hyp_body env sigma id in
604
if !check then recheck_typability (None,id) env' sigma cl;
607
let sign' = named_context_val (List.fold_left clear_aux env ids) in
608
let sg = mk_goal sign' cl in
611
| Move (withdep, hfrom, hto) ->
612
let (left,right,declfrom,toleft) =
613
split_sign hfrom hto (named_context_of_val sign) in
615
move_hyp withdep toleft (left,declfrom,right) hto in
616
([mk_goal hyps' cl], sigma)
619
let hyps' = reorder_val_context env sign ord in
620
([mk_goal hyps' cl], sigma)
622
| Rename (id1,id2) ->
623
if !check & id1 <> id2 &&
624
List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
625
error ((string_of_id id2)^" is already used.");
626
let sign' = rename_hyp id1 id2 sign in
627
let cl' = replace_vars [id1,mkVar id2] cl in
628
([mk_goal sign' cl'], sigma)
631
match norm_goal sigma goal with
632
Some ngl -> ([ngl],sigma)
633
| None -> ([goal], sigma)
635
(************************************************************************)
636
(************************************************************************)
637
(* Extracting a proof term from the proof tree *)
641
type variable_proof_status = ProofVar | SectionVar of identifier
643
type proof_variable = name * variable_proof_status
645
let subst_proof_vars =
648
List.fold_left (fun (n,l) var ->
649
let t = match var with
651
| Name id, ProofVar -> (id,mkRel n)::l
652
| Name id, SectionVar id' -> (id,mkVar id')::l in
654
in replace_vars (List.rev subst)
657
let rec rebind id1 id2 = function
658
| [] -> [Name id2,SectionVar id1]
660
if na = Name id1 then (Name id2,k)::l else
661
let l' = rebind id1 id2 l in
662
if na = Name id2 then (Anonymous,k)::l' else x::l'
664
let add_proof_var id vl = (Name id,ProofVar)::vl
666
let proof_variable_index x =
667
let rec aux n = function
668
| (Name id,ProofVar)::l when x = id -> n
669
| _::l -> aux (n+1) l
670
| [] -> raise Not_found
674
let prim_extractor subfun vl pft =
675
let cl = pft.goal.evar_concl in
677
| Some (Prim (Intro id), [spf]) ->
678
(match kind_of_term (strip_outer_cast cl) with
680
let cty = subst_proof_vars vl ty in
681
mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
682
| LetIn (_,b,ty,_) ->
683
let cb = subst_proof_vars vl b in
684
let cty = subst_proof_vars vl ty in
685
mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
686
| _ -> error "Incomplete proof!")
688
| Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) ->
689
let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
690
mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
691
subfun (add_proof_var id vl) spf2)
693
| Some (Prim (FixRule (f,n,others,j)),spfl) ->
694
let firsts,lasts = list_chop j others in
695
let all = Array.of_list (firsts@(f,n,cl)::lasts) in
696
let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
697
let names = Array.map (fun (f,_,_) -> Name f) all in
698
let vn = Array.map (fun (_,n,_) -> n-1) all in
699
let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
700
(add_proof_var f vl) others in
701
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
702
mkFix ((vn,j),(names,lcty,lfix))
704
| Some (Prim (Cofix (f,others,j)),spfl) ->
705
let firsts,lasts = list_chop j others in
706
let all = Array.of_list (firsts@(f,cl)::lasts) in
707
let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
708
let names = Array.map (fun (f,_) -> Name f) all in
709
let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
710
(add_proof_var f vl) others in
711
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
712
mkCoFix (j,(names,lcty,lfix))
714
| Some (Prim (Refine c),spfl) ->
715
let mvl = collect_meta_variables c in
716
let metamap = List.combine mvl (List.map (subfun vl) spfl) in
717
let cc = subst_proof_vars vl c in
718
plain_instance metamap cc
720
(* Structural and conversion rules do not produce any proof *)
721
| Some (Prim (Convert_concl (t,k)),[pf]) ->
722
if k = DEFAULTcast then subfun vl pf
723
else mkCast (subfun vl pf,k,subst_proof_vars vl cl)
724
| Some (Prim (Convert_hyp _),[pf]) ->
727
| Some (Prim (Thin _),[pf]) ->
728
(* No need to make ids Anon in vl: subst_proof_vars take the most recent*)
731
| Some (Prim (ThinBody _),[pf]) ->
734
| Some (Prim (Move _|Order _),[pf]) ->
737
| Some (Prim (Rename (id1,id2)),[pf]) ->
738
subfun (rebind id1 id2 vl) pf
740
| Some (Prim Change_evars, [pf]) ->
743
| Some _ -> anomaly "prim_extractor"
745
| None-> error "prim_extractor handed incomplete proof"
added
removed
proofs/logic.ml
