diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/gen_principle.ml | 10 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 1 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.mli | 2 |
4 files changed, 8 insertions, 7 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 73eb943418..67b6839b6e 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd : Evd.evar_map ref) interactive_proof fun_num tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef (fst fname) ) ] + , Tacred.EvalConstRef (fst fname) ) ] ; (let do_prove = build_proof interactive_proof (Array.to_list fnames) diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 314c8abcaf..c344fdd611 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -917,13 +917,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(1)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(1)) ) ] (destVar sigma args.(1), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -936,13 +936,13 @@ and intros_with_rewrite_aux () : unit Proofview.tactic = tclTHENLIST [ unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] ; tclMAP (fun id -> tclTRY (unfold_in_hyp [ ( Locus.AllOccurrences - , Names.EvalVarRef (destVar sigma args.(2)) ) ] + , Tacred.EvalVarRef (destVar sigma args.(2)) ) ] (destVar sigma args.(2), Locus.InHyp))) (pf_ids_of_hyps g) ; intros_with_rewrite () ] @@ -1158,7 +1158,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : else unfold_in_concl [ ( Locus.AllOccurrences - , Names.EvalConstRef + , Tacred.EvalConstRef (fst (destConst (Proofview.Goal.sigma g) f)) ) ] in (* The proof of each branche itself *) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 6464556e4e..266345a324 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -418,6 +418,7 @@ let make_eq () = with _ -> assert false let evaluable_of_global_reference r = + let open Tacred in (* Tacred.evaluable_of_global_reference (Global.env ()) *) match r with | GlobRef.ConstRef sp -> EvalConstRef sp diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 7b7044fdaf..e25f413fe4 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -100,7 +100,7 @@ val acc_rel : EConstr.constr Util.delayed val well_founded : EConstr.constr Util.delayed val evaluable_of_global_reference : - GlobRef.t -> Names.evaluable_global_reference + GlobRef.t -> Tacred.evaluable_global_reference val list_rewrite : bool -> (EConstr.constr * bool) list -> unit Proofview.tactic |