aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml3
-rw-r--r--plugins/cc/cctac.ml20
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml37
-rw-r--r--plugins/decl_mode/decl_proof_instr.mli2
-rw-r--r--plugins/firstorder/instances.ml18
-rw-r--r--plugins/firstorder/rules.ml27
-rw-r--r--plugins/fourier/fourierR.ml31
-rw-r--r--plugins/funind/functional_principles_proofs.ml42
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/g_indfun.ml410
-rw-r--r--plugins/funind/indfun.ml7
-rw-r--r--plugins/funind/invfun.ml44
-rw-r--r--plugins/funind/merge.ml9
-rw-r--r--plugins/funind/recdef.ml83
-rw-r--r--plugins/micromega/coq_micromega.ml14
-rw-r--r--plugins/nsatz/nsatz.ml1
-rw-r--r--plugins/omega/coq_omega.ml39
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--plugins/romega/refl_omega.ml9
-rw-r--r--plugins/rtauto/refl_tauto.ml1
-rw-r--r--plugins/ssrmatching/ssrmatching.ml41
21 files changed, 229 insertions, 183 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 1e49d8cad..27398cf65 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -249,9 +249,10 @@ module Btauto = struct
let fl = reify env fl in
let fr = reify env fr in
let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+ let changed_gl = EConstr.of_constr changed_gl in
Tacticals.New.tclTHENLIST [
Tactics.change_concl changed_gl;
- Tactics.apply (Lazy.force soundness);
+ Tactics.apply (EConstr.of_constr (Lazy.force soundness));
Tactics.normalise_vm_in_concl;
try_unification env
]
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7c78f3a17..7b023413d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -238,17 +238,17 @@ let build_projection intype (cstr:pconstructor) special default gls=
let _M =mkMeta
let app_global f args k =
- Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+ Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
let new_app_global f args k =
- Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
+ Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (EConstr.of_constr (mkApp (fc, args))))
-let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
-let refine c = refine (EConstr.of_constr c)
+let new_refine c = Proofview.V82.tactic (refine c)
+let refine c = refine c
let assert_before n c =
Proofview.Goal.enter { enter = begin fun gl ->
- let evm, _ = Tacmach.New.pf_apply type_of gl (EConstr.of_constr c) in
+ let evm, _ = Tacmach.New.pf_apply type_of gl c in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c)
end }
@@ -269,7 +269,7 @@ let rec proof_tac p : unit Proofview.tactic =
let type_of t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t) in
try (* type_of can raise exceptions *)
match p.p_rule with
- Ax c -> exact_check c
+ Ax c -> exact_check (EConstr.of_constr c)
| SymAx c ->
let l=constr_of_term p.p_lhs and
r=constr_of_term p.p_rhs in
@@ -333,6 +333,7 @@ let refute_tac c t1 t2 p =
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
let false_t=mkApp (c,[|mkVar hid|]) in
+ let false_t = EConstr.of_constr false_t in
let k intype =
let neweq= new_app_global _eq [|intype;tt1;tt2|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
@@ -341,7 +342,7 @@ let refute_tac c t1 t2 p =
end }
let refine_exact_check c gl =
- let evm, _ = pf_apply type_of gl (EConstr.of_constr c) in
+ let evm, _ = pf_apply type_of gl c in
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
@@ -363,6 +364,8 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
let tt2=constr_of_term t2 in
let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
let false_t=mkApp (c2,[|mkVar h|]) in
+ let false_t = EConstr.of_constr false_t in
+ let tt2 = EConstr.of_constr tt2 in
Tacticals.New.tclTHENS (assert_before (Name h) tt2)
[convert_to_goal_tac c1 t1 t2 p;
simplest_elim false_t]
@@ -387,6 +390,7 @@ let discriminate_tac (cstr,u as cstru) p =
[|intype;outtype;proj;t1;t2;mkVar hid|] in
let endt k =
injt (fun injt ->
+ let injt = EConstr.Unsafe.to_constr injt in
app_global _eq_rect
[|outtype;trivial;pred;identity;concl;injt|] k) in
let neweq=new_app_global _eq [|intype;t1;t2|] in
@@ -486,7 +490,7 @@ let mk_eq f c1 c2 k =
let term = mkApp (fc, [| ty; c1; c2 |]) in
let evm, _ = type_of (pf_env gl) evm (EConstr.of_constr term) in
Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
- (k term)
+ (k (EConstr.of_constr term))
end })
let f_equal =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 031a6253a..54206aa95 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -130,7 +130,7 @@ let clean_tmp gls =
clean_all (tmp_ids gls) gls
let assert_postpone id t =
- assert_before (Name id) t
+ assert_before (Name id) (EConstr.of_constr t)
(* start a proof *)
@@ -268,6 +268,7 @@ let add_justification_hyps keep items gls =
| _ ->
let id=pf_get_new_id local_hyp_prefix gls in
keep:=Id.Set.add id !keep;
+ let c = EConstr.of_constr c in
tclTHEN (Proofview.V82.of_tactic (letin_tac None (Names.Name id) c None Locusops.nowhere))
(Proofview.V82.of_tactic (clear_body [id])) gls in
tclMAP add_aux items gls
@@ -488,6 +489,7 @@ let thus_tac c ctyp submetas gls =
with Not_found ->
error "I could not relate this statement to the thesis." in
if List.is_empty list then
+ let proof = EConstr.of_constr proof in
Proofview.V82.of_tactic (exact_check proof) gls
else
let refiner = concl_refiner list proof gls in
@@ -546,7 +548,7 @@ let decompose_eq id gls =
let whd = (special_whd gls typ) in
match kind_of_term whd with
App (f,args)->
- if eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
+ if Term.eq_constr f (Lazy.force _eq) && Int.equal (Array.length args) 3
then (args.(0),
args.(1),
args.(2))
@@ -584,15 +586,15 @@ let instr_rew _thus rew_side cut gls0 =
let new_eq = mkApp(Lazy.force _eq,[|typ;cut.cut_stat.st_it;rhs|]) in
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity lhs))
- [just_tac;Proofview.V82.of_tactic (exact_check (mkVar last_id))]);
+ (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr lhs)))
+ [just_tac;Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id))]);
thus_tac new_eq] gls0
| Rhs ->
let new_eq = mkApp(Lazy.force _eq,[|typ;lhs;cut.cut_stat.st_it|]) in
tclTHENS (Proofview.V82.of_tactic (assert_postpone c_id new_eq))
[tclTHEN tcl_erase_info
- (tclTHENS (Proofview.V82.of_tactic (transitivity rhs))
- [Proofview.V82.of_tactic (exact_check (mkVar last_id));just_tac]);
+ (tclTHENS (Proofview.V82.of_tactic (transitivity (EConstr.of_constr rhs)))
+ [Proofview.V82.of_tactic (exact_check (EConstr.mkVar last_id));just_tac]);
thus_tac new_eq] gls0
@@ -772,7 +774,7 @@ let rec consider_match may_intro introduced available expected gls =
try conjunction_arity id gls with
Not_found -> error "Matching hypothesis not found." in
tclTHENLIST
- [Proofview.V82.of_tactic (simplest_case (mkVar id));
+ [Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id));
intron_then nhyps []
(fun l -> consider_match may_intro introduced
(List.rev_append l rest_ids) expected)] gls)
@@ -780,7 +782,8 @@ let rec consider_match may_intro introduced available expected gls =
gls
let consider_tac c hyps gls =
- match kind_of_term (strip_outer_cast (project gls) (EConstr.of_constr c)) with
+ let c = EConstr.of_constr c in
+ match kind_of_term (strip_outer_cast (project gls) c) with
Var id ->
consider_match false [] [id] hyps gls
| _ ->
@@ -817,6 +820,7 @@ let rec build_function sigma args body =
let define_tac id args body gls =
let t = build_function (project gls) args body in
+ let t = EConstr.of_constr t in
Proofview.V82.of_tactic (letin_tac None (Name id) t None Locusops.nowhere) gls
(* tactics for reconsider *)
@@ -828,6 +832,7 @@ let cast_tac id_or_thesis typ gls =
| Thesis (For _ ) ->
error "\"thesis for ...\" is not applicable here."
| Thesis Plain ->
+ let typ = EConstr.of_constr typ in
Proofview.V82.of_tactic (convert_concl typ DEFAULTcast) gls
(* per cases *)
@@ -1087,7 +1092,7 @@ let thesis_for obj typ per_info env=
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str"cannot give an induction hypothesis (wrong inductive type).") in
let params,args = List.chop per_info.per_nparams all_args in
- let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
+ let _ = if not (List.for_all2 Term.eq_constr params per_info.per_params) then
user_err ~hdr:"thesis_for"
((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
str "cannot give an induction hypothesis (wrong parameters).") in
@@ -1219,10 +1224,10 @@ let hrec_for fix_id per_info gls obj_id =
let ind,u = destInd cind in assert (eq_ind ind per_info.per_ind);
let params,args= List.chop per_info.per_nparams all_args in
assert begin
- try List.for_all2 eq_constr params per_info.per_params with
+ try List.for_all2 Term.eq_constr params per_info.per_params with
Invalid_argument _ -> false end;
let hd2 = applist (mkVar fix_id,args@[obj]) in
- compose_lam rc (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2))
+ EConstr.of_constr (compose_lam rc (Reductionops.whd_beta gls.sigma (EConstr.of_constr hd2)))
let warn_missing_case =
CWarnings.create ~name:"declmode-missing-case" ~category:"declmode"
@@ -1336,7 +1341,7 @@ let my_refine c gls =
let oc = { run = begin fun sigma ->
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = understand_my_constr (pf_env gls) sigma c (pf_concl gls) in
- Sigma.Unsafe.of_pair (c, sigma)
+ Sigma.Unsafe.of_pair (EConstr.of_constr c, sigma)
end } in
Proofview.V82.of_tactic (Tactics.New.refine oc) gls
@@ -1366,14 +1371,14 @@ let end_tac et2 gls =
begin
match et,ek with
_,EK_unknown ->
- tclSOLVE [Proofview.V82.of_tactic (simplest_elim pi.per_casee)]
+ tclSOLVE [Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr pi.per_casee))]
| ET_Case_analysis,EK_nodep ->
tclTHEN
- (Proofview.V82.of_tactic (simplest_case pi.per_casee))
+ (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr pi.per_casee)))
(default_justification (List.map mkVar clauses))
| ET_Induction,EK_nodep ->
tclTHENLIST
- [Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee]));
+ [Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee])));
Proofview.V82.of_tactic (simple_induct (AnonHyp (succ (List.length pi.per_args))));
default_justification (List.map mkVar clauses)]
| ET_Case_analysis,EK_dep tree ->
@@ -1385,7 +1390,7 @@ let end_tac et2 gls =
(initial_instance_stack clauses) [pi.per_casee] 0 tree
| ET_Induction,EK_dep tree ->
let nargs = (List.length pi.per_args) in
- tclTHEN (Proofview.V82.of_tactic (generalize (pi.per_args@[pi.per_casee])))
+ tclTHEN (Proofview.V82.of_tactic (generalize (List.map EConstr.of_constr (pi.per_args@[pi.per_casee]))))
begin
fun gls0 ->
let fix_id =
diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli
index 325969dad..ba196ff01 100644
--- a/plugins/decl_mode/decl_proof_instr.mli
+++ b/plugins/decl_mode/decl_proof_instr.mli
@@ -89,7 +89,7 @@ val push_arg : Term.constr ->
val hrec_for:
Id.t ->
Decl_mode.per_info -> Proof_type.goal Tacmach.sigma ->
- Id.t -> Term.constr
+ Id.t -> EConstr.constr
val consider_match :
bool ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 6c245063c..a320b47aa 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -117,6 +117,7 @@ let mk_open_instance id idc gl m t=
let nid=(fresh_id avoid var_id gl) in
let evmap = Sigma.Unsafe.of_evar_map evmap in
let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let c = EConstr.Unsafe.to_constr c in
let evmap = Sigma.to_evar_map evmap in
let decl = LocalAssum (Name nid, c) in
aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
@@ -131,13 +132,13 @@ let left_instance_tac (inst,id) continue seq=
if lookup (id,None) seq then
tclFAIL 0 (Pp.str "already done")
else
- tclTHENS (Proofview.V82.of_tactic (cut dom))
+ tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
pf_constr_of_global id (fun idc ->
(fun gls-> Proofview.V82.of_tactic (generalize
- [mkApp(idc,
- [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
+ [EConstr.of_constr (mkApp(idc,
+ [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls));
Proofview.V82.of_tactic introf;
tclSOLVE [wrap 1 false continue
(deepen (record (id,None) seq))]];
@@ -154,14 +155,15 @@ let left_instance_tac (inst,id) continue seq=
let gt=
it_mkLambda_or_LetIn
(mkApp(idc,[|ot|])) rc in
+ let gt = EConstr.of_constr gt in
let evmap, _ =
- try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
+ try Typing.type_of (pf_env gl) evmap gt
with e when CErrors.noncritical e ->
error "Untypable instance, maybe higher-order non-prenex quantification" in
tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
else
pf_constr_of_global id (fun idc ->
- Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
+ Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))]))
in
tclTHENLIST
[special_generalize;
@@ -172,16 +174,16 @@ let left_instance_tac (inst,id) continue seq=
let right_instance_tac inst continue seq=
match inst with
Phantom dom ->
- tclTHENS (Proofview.V82.of_tactic (cut dom))
+ tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
(fun gls->
Proofview.V82.of_tactic (split (ImplicitBindings
- [mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
+ [EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
tclSOLVE [wrap 0 true continue (deepen seq)]];
tclTRY (Proofview.V82.of_tactic assumption)]
| Real ((0,t),_) ->
- (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
+ (tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t])))
(tclSOLVE [wrap 0 true continue (deepen seq)]))
| Real ((m,t),_) ->
tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 1d107e9af..bed7a727f 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -59,7 +59,7 @@ let clear_global=function
(* connection rules *)
let axiom_tac t seq=
- try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
+ try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)))
with Not_found->tclFAIL 0 (Pp.str "No axiom link")
let ll_atom_tac a backtrack id continue seq=
@@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq=
tclTHENLIST
[pf_constr_of_global (find_left a seq) (fun left ->
pf_constr_of_global id (fun id ->
- Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
+ Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))])));
clear_global id;
Proofview.V82.of_tactic intro]
with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -95,7 +95,7 @@ let left_and_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
(tclTHENLIST
- [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
+ [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim));
clear_global id;
tclDO n (Proofview.V82.of_tactic intro)])
(wrap n false continue seq)
@@ -109,12 +109,12 @@ let left_or_tac ind backtrack id continue seq gls=
tclDO n (Proofview.V82.of_tactic intro);
wrap n false continue seq] in
tclIFTHENSVELSE
- (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
(Array.map f v)
backtrack gls
let left_false_tac id=
- Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
+ Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))
(* left arrow connective rules *)
@@ -131,7 +131,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let vars=Array.init p (fun j->mkRel (p-j)) in
let capply=mkApp ((lift p cstr),vars) in
let head=mkApp ((lift p idc),[|capply|]) in
- it_mkLambda_or_LetIn head rc in
+ EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
let lp=Array.length rcs in
let newhyps idc =List.init lp (myterm idc) in
tclIFTHENELSE
@@ -143,16 +143,16 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
let ll_arrow_tac a b c backtrack id continue seq=
let cc=mkProd(Anonymous,a,(lift 1 b)) in
- let d idc =mkLambda (Anonymous,b,
- mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+ let d idc =EConstr.of_constr (mkLambda (Anonymous,b,
+ mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in
tclORELSE
- (tclTHENS (Proofview.V82.of_tactic (cut c))
+ (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c)))
[tclTHENLIST
[Proofview.V82.of_tactic introf;
clear_global id;
wrap 1 false continue seq];
- tclTHENS (Proofview.V82.of_tactic (cut cc))
- [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
+ tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc)))
+ [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)));
tclTHENLIST
[pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
clear_global id;
@@ -177,7 +177,7 @@ let forall_tac backtrack continue seq=
let left_exists_tac ind backtrack id continue seq gls=
let n=(construct_nhyps ind gls).(0) in
tclIFTHENELSE
- (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+ (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
(tclTHENLIST [clear_global id;
tclDO n (Proofview.V82.of_tactic intro);
(wrap (n-1) false continue seq)])
@@ -186,13 +186,14 @@ let left_exists_tac ind backtrack id continue seq gls=
let ll_forall_tac prod backtrack id continue seq=
tclORELSE
- (tclTHENS (Proofview.V82.of_tactic (cut prod))
+ (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod)))
[tclTHENLIST
[Proofview.V82.of_tactic intro;
pf_constr_of_global id (fun idc ->
(fun gls->
let id0=pf_nth_hyp_id gls 1 in
let term=mkApp(idc,[|mkVar(id0)|]) in
+ let term = EConstr.of_constr term in
tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
clear_global id;
Proofview.V82.of_tactic intro;
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a14ec8a2c..fa64b276c 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -281,6 +281,8 @@ let fourier_lineq lineq1 =
(* Defined constants *)
let get = Lazy.force
+let cget = get
+let eget c = EConstr.of_constr (Lazy.force c)
let constant = Coqlib.gen_constant "Fourier"
(* Standard library *)
@@ -373,6 +375,7 @@ let rational_to_real x =
(* preuve que 0<n*1/d
*)
let tac_zero_inf_pos gl (n,d) =
+ let get = eget in
let tacn=ref (apply (get coq_Rlt_zero_1)) in
let tacd=ref (apply (get coq_Rlt_zero_1)) in
for _i = 1 to n - 1 do
@@ -385,6 +388,7 @@ let tac_zero_inf_pos gl (n,d) =
(* preuve que 0<=n*1/d
*)
let tac_zero_infeq_pos gl (n,d)=
+ let get = eget in
let tacn=ref (if n=0
then (apply (get coq_Rle_zero_zero))
else (apply (get coq_Rle_zero_1))) in
@@ -399,7 +403,8 @@ let tac_zero_infeq_pos gl (n,d)=
(* preuve que 0<(-n)*(1/d) => False
*)
let tac_zero_inf_false gl (n,d) =
- if n=0 then (apply (get coq_Rnot_lt0))
+ let get = eget in
+if n=0 then (apply (get coq_Rnot_lt0))
else
(Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
(tac_zero_infeq_pos gl (-n,d)))
@@ -408,6 +413,7 @@ let tac_zero_inf_false gl (n,d) =
(* preuve que 0<=(-n)*(1/d) => False
*)
let tac_zero_infeq_false gl (n,d) =
+ let get = eget in
(Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
(tac_zero_inf_pos gl (-n,d)))
;;
@@ -415,7 +421,8 @@ let tac_zero_infeq_false gl (n,d) =
let exact = exact_check;;
let tac_use h =
- let tac = exact h.hname in
+ let get = eget in
+ let tac = exact (EConstr.of_constr h.hname) in
match h.htype with
"Rlt" -> tac
|"Rle" -> tac
@@ -470,6 +477,7 @@ let rec fourier () =
try
match (kind_of_term goal) with
App (f,args) ->
+ let get = eget in
(match (string_of_R_constr f) with
"Rlt" ->
(Tacticals.New.tclTHEN
@@ -548,6 +556,7 @@ let rec fourier () =
!t2 |] in
let tc=rational_to_real cres in
(* puis sa preuve *)
+ let get = eget in
let tac1=ref (if h1.hstrict
then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
[tac_use h1;
@@ -584,29 +593,29 @@ let rec fourier () =
then tac_zero_inf_false gl (rational_to_fraction cres)
else tac_zero_infeq_false gl (rational_to_fraction cres)
in
- tac:=(Tacticals.New.tclTHENS (cut ineq)
+ tac:=(Tacticals.New.tclTHENS (cut (EConstr.of_constr ineq))
[Tacticals.New.tclTHEN (change_concl
- (mkAppL [| get coq_not; ineq|]
- ))
+ (EConstr.of_constr (mkAppL [| cget coq_not; ineq|]
+ )))
(Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
else get coq_Rnot_le_le))
(Tacticals.New.tclTHENS (Equality.replace
- (mkAppL [|get coq_Rminus;!t2;!t1|]
+ (mkAppL [|cget coq_Rminus;!t2;!t1|]
)
tc)
[tac2;
(Tacticals.New.tclTHENS
(Equality.replace
- (mkApp (get coq_Rinv,
- [|get coq_R1|]))
- (get coq_R1))
+ (mkApp (cget coq_Rinv,
+ [|cget coq_R1|]))
+ (cget coq_R1))
(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
[Tacticals.New.tclORELSE
(* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
(Proofview.tclUNIT ());
- Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
- (Tacticals.New.tclTHEN (apply symeq)
+ Tacticals.New.pf_constr_of_global (cget coq_sym_eqT) (fun symeq ->
+ (Tacticals.New.tclTHEN (apply (EConstr.of_constr symeq))
(apply (get coq_Rinv_1))))]
)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b674f40e9..503cafdd5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -175,6 +175,7 @@ let is_incompatible_eq t =
res
let change_hyp_with_using msg hyp_id t tac : tactic =
+ let t = EConstr.of_constr t in
fun g ->
let prov_id = pf_get_new_id hyp_id g in
tclTHENS
@@ -451,6 +452,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
)
in
let to_refine = EConstr.of_constr to_refine in
+ let t_x = EConstr.of_constr t_x in
(* observe_tac "rec hyp " *)
(tclTHENS
(Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
@@ -644,7 +646,8 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
fun g ->
let prov_hid = pf_get_new_id hid g in
let c = mkApp(mkVar hid,args) in
- let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr c) in
+ let c = EConstr.of_constr c in
+ let evm, _ = pf_apply Typing.type_of g c in
tclTHENLIST[
Refiner.tclEVARS evm;
Proofview.V82.of_tactic (pose_proof (Name prov_hid) c);
@@ -709,13 +712,14 @@ let build_proof
let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t
in
+ let term_eq = EConstr.of_constr term_eq in
tclTHENSEQ
[
- Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
+ Proofview.V82.of_tactic (generalize (term_eq::(List.map EConstr.mkVar dyn_infos.rec_hyps)));
thin dyn_infos.rec_hyps;
- Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
+ Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],EConstr.of_constr t] None);
(fun g -> observe_tac "toto" (
- tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
+ tclTHENSEQ [Proofview.V82.of_tactic (Simple.case (EConstr.of_constr t));
(fun g' ->
let g'_nb_prod = nb_prod (project g') (EConstr.of_constr (pf_concl g')) in
let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -942,7 +946,7 @@ let generalize_non_dep hyp g =
in
(* observe (str "to_revert := " ++ prlist_with_sep spc Ppconstr.pr_id to_revert); *)
tclTHEN
- ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize (List.map mkVar to_revert) )))
+ ((* observe_tac "h_generalize" *) (Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar to_revert) )))
((* observe_tac "thin" *) (thin to_revert))
g
@@ -950,7 +954,7 @@ let id_of_decl = RelDecl.get_name %> Nameops.out_name
let var_of_decl = id_of_decl %> mkVar
let revert idl =
tclTHEN
- (Proofview.V82.of_tactic (generalize (List.map mkVar idl)))
+ (Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar idl)))
(thin idl)
let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num =
@@ -991,7 +995,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
let rec_id = pf_nth_hyp_id g 1 in
tclTHENSEQ
[observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
- observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
+ observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar rec_id)));
(Proofview.V82.of_tactic intros_reflexivity)] g
)
]
@@ -1064,10 +1068,11 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnames all_funs _nparams : tactic =
fun g ->
let princ_type = pf_concl g in
+ let princ_type = EConstr.of_constr princ_type in
(* Pp.msgnl (str "princ_type " ++ Printer.pr_lconstr princ_type); *)
(* Pp.msgnl (str "all_funs "); *)
(* Array.iter (fun c -> Pp.msgnl (Printer.pr_lconstr c)) all_funs; *)
- let princ_info = compute_elim_sig princ_type in
+ let princ_info = compute_elim_sig (project g) princ_type in
let fresh_id =
let avoid = ref (pf_ids_of_hyps g) in
(fun na ->
@@ -1227,7 +1232,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
| _, this_fix_info::others_infos ->
let other_fix_infos =
List.map
- (fun fi -> fi.name,fi.idx + 1 ,fi.types)
+ (fun fi -> fi.name,fi.idx + 1 ,EConstr.of_constr fi.types)
(pre_info@others_infos)
in
if List.is_empty other_fix_infos
@@ -1462,11 +1467,11 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
backtrack_eqs_until_hrec hrec eqs;
(* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
(tclTHENS (* We must have exactly ONE subgoal !*)
- (Proofview.V82.of_tactic (apply (mkVar hrec)))
+ (Proofview.V82.of_tactic (apply (EConstr.mkVar hrec)))
[ tclTHENSEQ
[
(Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
- (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
+ (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force acc_inv))));
(fun g ->
if is_mes
then
@@ -1482,7 +1487,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
tclCOMPLETE(
Eauto.eauto_with_bases
(true,5)
- [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
)
)
@@ -1518,7 +1523,8 @@ let prove_principle_for_gen
(f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes
rec_arg_num rec_arg_type relation gl =
let princ_type = pf_concl gl in
- let princ_info = compute_elim_sig princ_type in
+ let princ_type = EConstr.of_constr princ_type in
+ let princ_info = compute_elim_sig (project gl) princ_type in
let fresh_id =
let avoid = ref (pf_ids_of_hyps gl) in
fun na ->
@@ -1572,7 +1578,7 @@ let prove_principle_for_gen
Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
in
let revert l =
- tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map mkVar l))) (Proofview.V82.of_tactic (clear l))
+ tclTHEN (Proofview.V82.of_tactic (Tactics.generalize (List.map EConstr.mkVar l))) (Proofview.V82.of_tactic (clear l))
in
let fix_id = Nameops.out_name (fresh_id (Name hrec_id)) in
let prove_rec_arg_acc g =
@@ -1580,12 +1586,12 @@ let prove_principle_for_gen
(tclCOMPLETE
(tclTHEN
(Proofview.V82.of_tactic (assert_by (Name wf_thm_id)
- (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
(Proofview.V82.tactic (fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g))))
(
(* observe_tac *)
(* "apply wf_thm" *)
- Proofview.V82.of_tactic (Tactics.Simple.apply (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|])))
+ Proofview.V82.of_tactic (Tactics.Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm_id,[|mkVar rec_arg_id|]))))
)
)
)
@@ -1596,7 +1602,7 @@ let prove_principle_for_gen
let lemma =
match !tcc_lemma_ref with
| None -> error "No tcc proof !!"
- | Some lemma -> lemma
+ | Some lemma -> EConstr.of_constr lemma
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
@@ -1644,7 +1650,7 @@ let prove_principle_for_gen
);
(* observe_tac "" *) Proofview.V82.of_tactic (assert_by
(Name acc_rec_arg_id)
- (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
+ (EConstr.of_constr (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|])))
(Proofview.V82.tactic prove_rec_arg_acc)
);
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 4b47b83af..4d88f9f91 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -28,7 +28,8 @@ let observe s =
a functional one
*)
let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
- let princ_type_info = compute_elim_sig princ_type in
+ let princ_type = EConstr.of_constr princ_type in
+ let princ_type_info = compute_elim_sig Evd.empty princ_type (** FIXME *) in
let env = Global.env () in
let env_with_params = Environ.push_rel_context princ_type_info.params env in
let tbl = Hashtbl.create 792 in
@@ -89,7 +90,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
(Option.fold_right
mkProd_or_LetIn
princ_type_info.indarg
- princ_type_info.concl
+ (EConstr.Unsafe.to_constr princ_type_info.concl)
)
princ_type_info.args
)
@@ -243,7 +244,8 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let change_property_sort evd toSort princ princName =
let open Context.Rel.Declaration in
- let princ_info = compute_elim_sig princ in
+ let princ = EConstr.of_constr princ in
+ let princ_info = compute_elim_sig evd princ in
let change_sort_in_predicate decl =
LocalAssum
(get_name decl,
@@ -270,7 +272,7 @@ let change_property_sort evd toSort princ princName =
let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
(* First we get the type of the old graph principle *)
- let mutr_nparams = (compute_elim_sig old_princ_type).nparams in
+ let mutr_nparams = (compute_elim_sig !evd (EConstr.of_constr old_princ_type)).nparams in
(* let time1 = System.get_time () in *)
let new_principle_type =
compute_new_princ_type_from_rel
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a8..a6f971703 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -58,7 +58,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
| None -> mt ()
| Some b ->
let (b, _) = Tactics.run_delayed (Global.env ()) Evd.empty b in
- spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b)
+ spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed (EConstr.Unsafe.to_constr %> prc) (EConstr.Unsafe.to_constr %> prlc) b)
ARGUMENT EXTEND fun_ind_using
@@ -97,7 +97,9 @@ ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [] ->[ None ]
END
-
+let functional_induction b c x pat =
+ let x = Option.map (Miscops.map_with_bindings EConstr.Unsafe.to_constr) x in
+ Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
TACTIC EXTEND newfunind
@@ -108,7 +110,7 @@ TACTIC EXTEND newfunind
| [c] -> c
| c::cl -> applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))) princl ]
+ Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
END
(***** debug only ***)
TACTIC EXTEND snewfunind
@@ -119,7 +121,7 @@ TACTIC EXTEND snewfunind
| [c] -> c
| c::cl -> applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> Proofview.V82.tactic (functional_induction false c x (Option.map out_disjunctive pat))) princl ]
+ Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e3ba52246..37a76bec1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -81,7 +81,8 @@ let functional_induction with_clean c princl pat =
| Some ((princ,binding)) ->
princ,binding,Tacmach.pf_unsafe_type_of g (EConstr.of_constr princ),g
in
- let princ_infos = Tactics.compute_elim_sig princ_type in
+ let princ_type = EConstr.of_constr princ_type in
+ let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
let args_as_induction_constr =
let c_list =
if princ_infos.Tactics.farg_in_concl
@@ -89,9 +90,11 @@ let functional_induction with_clean c princl pat =
in
let encoded_pat_as_patlist =
List.make (List.length args + List.length c_list - 1) None @ [pat] in
- List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
+ List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr ({ Tacexpr.delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) })),(None,pat),None))
(args@c_list) encoded_pat_as_patlist
in
+ let princ = EConstr.of_constr princ in
+ let bindings = Miscops.map_bindings EConstr.of_constr bindings in
let princ' = Some (princ,bindings) in
let princ_vars =
List.fold_right
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b2419b1a5..36fb6dad3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* and the principle to use in this lemma in $\zeta$ normal form *)
let f_principle,princ_type = schemes.(i) in
let princ_type = nf_zeta (EConstr.of_constr princ_type) in
- let princ_infos = Tactics.compute_elim_sig princ_type in
+ let princ_type = EConstr.of_constr princ_type in
+ let princ_infos = Tactics.compute_elim_sig evd princ_type in
(* The number of args of the function is then easily computable *)
let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
@@ -315,7 +316,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
match kind_of_term t'',kind_of_term t''' with
| App(eq,args), App(graph',_)
when
- (eq_constr eq eq_ind) &&
+ (Term.eq_constr eq eq_ind) &&
Array.exists (Constr.eq_constr_nounivs graph') graphs_constr ->
(args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
::acc)
@@ -387,7 +388,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
(* Conclusion *)
observe_tac "exact" (fun g ->
- Proofview.V82.of_tactic (exact_check (app_constructor g)) g)
+ Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)
]
)
g
@@ -440,7 +441,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
observe_tac "principle" (Proofview.V82.of_tactic (assert_by
(Name principle_id)
princ_type
- (exact_check f_principle)));
+ (exact_check (EConstr.of_constr f_principle))));
observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
observe_tac "idtac" tclIDTAC;
@@ -450,7 +451,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(fun gl ->
let term = mkApp (mkVar principle_id,Array.of_list bindings) in
let gl', _ty = pf_eapply (Typing.type_of ~refresh:true) gl (EConstr.of_constr term) in
- Proofview.V82.of_tactic (apply term) gl')
+ Proofview.V82.of_tactic (apply (EConstr.of_constr term)) gl')
))
(fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
]
@@ -467,7 +468,7 @@ let generalize_dependent_of x hyp g =
tclMAP
(function
| LocalAssum (id,t) when not (Id.equal id hyp) &&
- (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+ (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (thin [id])
| _ -> tclIDTAC
)
(pf_hyps g)
@@ -495,7 +496,7 @@ and intros_with_rewrite_aux : tactic =
| Prod(_,t,t') ->
begin
match kind_of_term t with
- | App(eq,args) when (eq_constr eq eq_ind) ->
+ | App(eq,args) when (Term.eq_constr eq eq_ind) ->
if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
then
let id = pf_get_new_id (Id.of_string "y") g in
@@ -541,11 +542,11 @@ and intros_with_rewrite_aux : tactic =
intros_with_rewrite
] g
end
- | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
+ | Ind _ when Term.eq_constr t (Coqlib.build_coq_False ()) ->
Proofview.V82.of_tactic tauto g
| Case(_,_,v,_) ->
tclTHENSEQ[
- Proofview.V82.of_tactic (simplest_case v);
+ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
intros_with_rewrite
] g
| LetIn _ ->
@@ -582,7 +583,7 @@ let rec reflexivity_with_destruct_cases g =
match kind_of_term (snd (destApp (pf_concl g))).(2) with
| Case(_,_,v,_) ->
tclTHENSEQ[
- Proofview.V82.of_tactic (simplest_case v);
+ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
Proofview.V82.of_tactic intros;
observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
]
@@ -597,7 +598,7 @@ let rec reflexivity_with_destruct_cases g =
None -> tclIDTAC g
| Some id ->
match kind_of_term (pf_unsafe_type_of g (EConstr.mkVar id)) with
- | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
+ | App(eq,[|_;t1;t2|]) when Term.eq_constr eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
then Proofview.V82.of_tactic (Equality.discrHyp id) g
else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
@@ -662,7 +663,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let f = funcs.(i) in
let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in
let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
- let princ_infos = Tactics.compute_elim_sig princ_type in
+ let princ_type = EConstr.of_constr princ_type in
+ let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
(* Then we get the number of argument of the function
and compute a fresh name for each of them
*)
@@ -717,7 +719,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
})
Locusops.onConcl)
;
- Proofview.V82.of_tactic (generalize (List.map mkVar ids));
+ Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar ids));
thin ids
]
else
@@ -756,10 +758,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
tclTHENSEQ
[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
observe_tac "h_generalize"
- (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
+ (Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
Proofview.V82.of_tactic (Simple.intro graph_principle_id);
observe_tac "" (tclTHEN_i
- (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+ (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
(fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
]
g
@@ -939,7 +941,7 @@ let revert_graph kn post_tac hid g =
let f_args,res = Array.chop (Array.length args - 1) args in
tclTHENSEQ
[
- Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
+ Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid]))]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
post_tac hid
@@ -972,18 +974,18 @@ let functional_inversion kn hid fconst f_correct : tactic =
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
match kind_of_term type_of_h with
- | App(eq,args) when eq_constr eq (make_eq ()) ->
+ | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
let pre_tac,f_args,res =
match kind_of_term args.(1),kind_of_term args.(2) with
- | App(f,f_args),_ when eq_constr f fconst ->
+ | App(f,f_args),_ when Term.eq_constr f fconst ->
((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
- |_,App(f,f_args) when eq_constr f fconst ->
+ |_,App(f,f_args) when Term.eq_constr f fconst ->
((fun hid -> tclIDTAC),f_args,args.(1))
| _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
in
tclTHENSEQ[
pre_tac hid;
- Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
+ Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(f_correct,(Array.to_list f_args)@[res;mkVar hid]))]);
thin [hid];
Proofview.V82.of_tactic (Simple.intro hid);
Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
@@ -1024,7 +1026,7 @@ let invfun qhyp f g =
(fun hid -> Proofview.V82.tactic begin fun g ->
let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
match kind_of_term hyp_typ with
- | App(eq,args) when eq_constr eq (make_eq ()) ->
+ | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
begin
let f1,_ = decompose_app args.(1) in
try
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 222c0c804..3688b8c15 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -32,7 +32,7 @@ module RelDecl = Context.Rel.Declaration
(** {2 Useful operations on constr and glob_constr} *)
-let rec popn i c = if i<=0 then c else pop (EConstr.of_constr (popn (i-1) c))
+let rec popn i c = if i<=0 then c else EConstr.of_constr (pop (popn (i-1) c))
(** Substitutions in constr *)
let compare_constr_nosub t1 t2 =
@@ -979,19 +979,20 @@ let funify_branches relinfo nfuns branch =
let relprinctype_to_funprinctype relprinctype nfuns =
- let relinfo = compute_elim_sig relprinctype in
+ let relprinctype = EConstr.of_constr relprinctype in
+ let relinfo = compute_elim_sig Evd.empty (** FIXME*) relprinctype in
assert (not relinfo.farg_in_concl);
assert (relinfo.indarg_in_concl);
(* first remove indarg and indarg_in_concl *)
let relinfo_noindarg = { relinfo with
indarg_in_concl = false; indarg = None;
- concl = remove_last_arg (pop (EConstr.of_constr relinfo.concl)); } in
+ concl = EConstr.of_constr (remove_last_arg (pop relinfo.concl)); } in
(* the nfuns last induction arguments are functional ones: remove them *)
let relinfo_argsok = { relinfo_noindarg with
nargs = relinfo_noindarg.nargs - nfuns;
(* args is in reverse order, so remove fst *)
args = remove_n_fst_list nfuns relinfo_noindarg.args;
- concl = popn nfuns relinfo_noindarg.concl
+ concl = popn nfuns relinfo_noindarg.concl;
} in
let new_branches =
List.map (funify_branches relinfo_argsok nfuns) relinfo_argsok.branches in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b2c93a754..d5ee42af8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -286,7 +286,7 @@ let tclUSER tac is_mes l g =
let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
if is_mes
- then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (delayed_force well_founded_ltof)) gl)
+ then tclCOMPLETE (fun gl -> Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (delayed_force well_founded_ltof))) gl)
else (* tclTHEN (Simple.apply (delayed_force acc_intro_generator_function) ) *) (tclUSER concl_tac is_mes names_to_suppress)
@@ -465,7 +465,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
end
| App _ ->
let f,args = decompose_app expr_info.info in
- if eq_constr f (expr_info.f_constr)
+ if Term.eq_constr f (expr_info.f_constr)
then jinfo.app_reC (f,args) expr_info continuation_tac expr_info
else
begin
@@ -517,21 +517,21 @@ let rec prove_lt hyple g =
let h =
List.find (fun id ->
match decompose_app (pf_unsafe_type_of g (EConstr.mkVar id)) with
- | _, t::_ -> eq_constr t varx
+ | _, t::_ -> Term.eq_constr t varx
| _ -> false
) hyple
in
let y =
List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (EConstr.mkVar h))))) in
observe_tclTHENLIST (str "prove_lt1")[
- Proofview.V82.of_tactic (apply (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|])));
+ Proofview.V82.of_tactic (apply (EConstr.of_constr (mkApp(le_lt_trans (),[|varx;y;varz;mkVar h|]))));
observe_tac (str "prove_lt") (prove_lt hyple)
]
with Not_found ->
(
(
observe_tclTHENLIST (str "prove_lt2")[
- Proofview.V82.of_tactic (apply (delayed_force lt_S_n));
+ Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force lt_S_n)));
(observe_tac (str "assumption: " ++ Printer.pr_goal g) (Proofview.V82.of_tactic assumption))
])
)
@@ -549,15 +549,15 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
let ids = h'::ids in
let def = next_ident_away_in_goal def_id ids in
observe_tclTHENLIST (str "destruct_bounds_aux1")[
- Proofview.V82.of_tactic (split (ImplicitBindings [s_max]));
+ Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr s_max]));
Proofview.V82.of_tactic (intro_then
(fun id ->
Proofview.V82.tactic begin
observe_tac (str "destruct_bounds_aux")
- (tclTHENS (Proofview.V82.of_tactic (simplest_case (mkVar id)))
+ (tclTHENS (Proofview.V82.of_tactic (simplest_case (EConstr.mkVar id)))
[
observe_tclTHENLIST (str "")[Proofview.V82.of_tactic (intro_using h_id);
- Proofview.V82.of_tactic (simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|])));
+ Proofview.V82.of_tactic (simplest_elim(EConstr.of_constr (mkApp(delayed_force lt_n_O,[|s_max|]))));
Proofview.V82.of_tactic default_full_auto];
observe_tclTHENLIST (str "destruct_bounds_aux2")[
observe_tac (str "clearing k ") (Proofview.V82.of_tactic (clear [id]));
@@ -588,7 +588,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
] g
| (_,v_bound)::l ->
observe_tclTHENLIST (str "destruct_bounds_aux3")[
- Proofview.V82.of_tactic (simplest_elim (mkVar v_bound));
+ Proofview.V82.of_tactic (simplest_elim (EConstr.mkVar v_bound));
Proofview.V82.of_tactic (clear [v_bound]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1
@@ -597,7 +597,7 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
(fun p ->
observe_tclTHENLIST (str "destruct_bounds_aux4")[
Proofview.V82.of_tactic (simplest_elim
- (mkApp(delayed_force max_constr, [| bound; mkVar p|])));
+ (EConstr.of_constr (mkApp(delayed_force max_constr, [| bound; mkVar p|]))));
tclDO 3 (Proofview.V82.of_tactic intro);
onNLastHypsId 3 (fun lids ->
match lids with
@@ -622,7 +622,7 @@ let terminate_app f_and_args expr_info continuation_tac infos =
observe_tclTHENLIST (str "terminate_app1")[
continuation_tac infos;
observe_tac (str "first split")
- (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+ (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
]
else continuation_tac infos
@@ -633,7 +633,7 @@ let terminate_others _ expr_info continuation_tac infos =
observe_tclTHENLIST (str "terminate_others")[
continuation_tac infos;
observe_tac (str "first split")
- (Proofview.V82.of_tactic (split (ImplicitBindings [infos.info])));
+ (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr infos.info])));
observe_tac (str "destruct_bounds") (destruct_bounds infos)
]
else continuation_tac infos
@@ -657,7 +657,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
let pf_type c tac gl =
- let evars, ty = Typing.type_of (pf_env gl) (project gl) (EConstr.of_constr c) in
+ let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
let pf_typel l tac =
@@ -687,16 +687,18 @@ let mkDestructEq :
let type_of_expr = pf_unsafe_type_of g (EConstr.of_constr expr) in
let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
to_revert_constr in
+ let new_hyps = List.map EConstr.of_constr new_hyps in
pf_typel new_hyps (fun _ ->
observe_tclTHENLIST (str "mkDestructEq")
[Proofview.V82.of_tactic (generalize new_hyps);
(fun g2 ->
let changefun patvars = { run = fun sigma ->
let redfun = pattern_occs [Locus.AllOccurrencesBut [1], EConstr.of_constr expr] in
- redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
+ let Sigma (c, sigma, p) = redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2)) in
+ Sigma (EConstr.of_constr c, sigma, p)
} in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
- Proofview.V82.of_tactic (simplest_case expr)]), to_revert
+ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr expr))]), to_revert
let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
@@ -742,7 +744,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
then
observe_tclTHENLIST (str "terminate_app_rec1")[
observe_tac (str "first split")
- (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+ (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
observe_tac (str "destruct_bounds (3)")
(destruct_bounds new_infos)
]
@@ -751,7 +753,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
]
with Not_found ->
observe_tac (str "terminate_app_rec not found") (tclTHENS
- (Proofview.V82.of_tactic (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args))))
+ (Proofview.V82.of_tactic (simplest_elim (EConstr.of_constr (mkApp(mkVar expr_info.ih,Array.of_list args)))))
[
observe_tclTHENLIST (str "terminate_app_rec2")[
Proofview.V82.of_tactic (intro_using rec_res_id);
@@ -772,7 +774,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
then
observe_tclTHENLIST (str "terminate_app_rec4")[
observe_tac (str "first split")
- (Proofview.V82.of_tactic (split (ImplicitBindings [new_infos.info])));
+ (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr new_infos.info])));
observe_tac (str "destruct_bounds (2)")
(destruct_bounds new_infos)
]
@@ -785,7 +787,7 @@ let terminate_app_rec (f,args) expr_info continuation_tac _ =
];
observe_tac (str "proving decreasing") (
tclTHENS (* proof of args < formal args *)
- (Proofview.V82.of_tactic (apply (Lazy.force expr_info.acc_inv)))
+ (Proofview.V82.of_tactic (apply (EConstr.of_constr (Lazy.force expr_info.acc_inv))))
[
observe_tac (str "assumption") (Proofview.V82.of_tactic assumption);
observe_tclTHENLIST (str "terminate_app_rec5")
@@ -833,7 +835,7 @@ let rec prove_le g =
in
tclFIRST[
Proofview.V82.of_tactic assumption;
- Proofview.V82.of_tactic (apply (delayed_force le_n));
+ Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_n)));
begin
try
let matching_fun =
@@ -846,7 +848,7 @@ let rec prove_le g =
List.hd (List.tl args)
in
observe_tclTHENLIST (str "prove_le")[
- Proofview.V82.of_tactic (apply(mkApp(le_trans (),[|x;y;z;mkVar h|])));
+ Proofview.V82.of_tactic (apply(EConstr.of_constr (mkApp(le_trans (),[|x;y;z;mkVar h|]))));
observe_tac (str "prove_le (rec)") (prove_le)
]
with Not_found -> tclFAIL 0 (mt())
@@ -876,7 +878,7 @@ let rec make_rewrite_list expr_info max = function
)
[make_rewrite_list expr_info max l;
observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
- Proofview.V82.of_tactic (apply (delayed_force le_lt_n_Sm));
+ Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_n_Sm)));
observe_tac (str "prove_le(2)") prove_le
]
] )
@@ -916,7 +918,7 @@ let make_rewrite expr_info l hp max =
]))
;
observe_tclTHENLIST (str "make_rewrite1")[ (* x < S (S max) proof *)
- Proofview.V82.of_tactic (apply (delayed_force le_lt_SS));
+ Proofview.V82.of_tactic (apply (EConstr.of_constr (delayed_force le_lt_SS)));
observe_tac (str "prove_le (3)") prove_le
]
])
@@ -928,7 +930,7 @@ let rec compute_max rew_tac max l =
| (_,p,_)::l ->
observe_tclTHENLIST (str "compute_max")[
Proofview.V82.of_tactic (simplest_elim
- (mkApp(delayed_force max_constr, [| max; mkVar p|])));
+ (EConstr.of_constr (mkApp(delayed_force max_constr, [| max; mkVar p|]))));
tclDO 3 (Proofview.V82.of_tactic intro);
onNLastHypsId 3 (fun lids ->
match lids with
@@ -947,7 +949,7 @@ let rec destruct_hex expr_info acc l =
end
| (v,hex)::l ->
observe_tclTHENLIST (str "destruct_hex")[
- Proofview.V82.of_tactic (simplest_case (mkVar hex));
+ Proofview.V82.of_tactic (simplest_case (EConstr.mkVar hex));
Proofview.V82.of_tactic (clear [hex]);
tclDO 2 (Proofview.V82.of_tactic intro);
onNthHypId 1 (fun hp ->
@@ -995,13 +997,13 @@ let equation_app_rec (f,args) expr_info continuation_tac info =
if expr_info.is_final && expr_info.is_main_branch
then
observe_tclTHENLIST (str "equation_app_rec")
- [ Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+ [ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
]
else
observe_tclTHENLIST (str "equation_app_rec1")[
- Proofview.V82.of_tactic (simplest_case (mkApp (expr_info.f_terminate,Array.of_list args)));
+ Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (expr_info.f_terminate,Array.of_list args))));
observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
]
end
@@ -1086,9 +1088,9 @@ let termination_proof_header is_mes input_type ids args_id relation
(str "first assert")
(Proofview.V82.of_tactic (assert_before
(Name wf_rec_arg)
- (mkApp (delayed_force acc_rel,
+ (EConstr.of_constr (mkApp (delayed_force acc_rel,
[|input_type;relation;mkVar rec_arg_id|])
- )
+ ))
))
)
[
@@ -1098,7 +1100,7 @@ let termination_proof_header is_mes input_type ids args_id relation
(str "second assert")
(Proofview.V82.of_tactic (assert_before
(Name wf_thm)
- (mkApp (delayed_force well_founded,[|input_type;relation|]))
+ (EConstr.of_constr (mkApp (delayed_force well_founded,[|input_type;relation|])))
))
)
[
@@ -1107,7 +1109,7 @@ let termination_proof_header is_mes input_type ids args_id relation
(* this gives the accessibility argument *)
observe_tac
(str "apply wf_thm")
- (Proofview.V82.of_tactic (Simple.apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|])))
+ (Proofview.V82.of_tactic (Simple.apply (EConstr.of_constr (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))))
)
]
;
@@ -1116,7 +1118,7 @@ let termination_proof_header is_mes input_type ids args_id relation
[observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
- tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
+ tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (Proofview.V82.of_tactic (clear [id])))
))
;
observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
@@ -1214,7 +1216,7 @@ let build_and_l l =
| Prod(_,_,t') -> is_well_founded t'
| App(_,_) ->
let (f,_) = decompose_app t in
- eq_constr f (well_founded ())
+ Term.eq_constr f (well_founded ())
| _ ->
false
in
@@ -1231,7 +1233,7 @@ let build_and_l l =
let c,tac,nb = f pl in
mk_and p1 c,
tclTHENS
- (Proofview.V82.of_tactic (apply (constr_of_global conj_constr)))
+ (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr))))
[tclIDTAC;
tac
],nb+1
@@ -1297,6 +1299,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
ref_ := Some lemma ;
+ let lemma = EConstr.of_constr lemma in
let lid = ref [] in
let h_num = ref (-1) in
let env = Global.env () in
@@ -1323,7 +1326,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
] gls)
(fun g ->
match kind_of_term (pf_concl g) with
- | App(f,_) when eq_constr f (well_founded ()) ->
+ | App(f,_) when Term.eq_constr f (well_founded ()) ->
Proofview.V82.of_tactic (Auto.h_auto None [] (Some [])) g
| _ ->
incr h_num;
@@ -1332,11 +1335,11 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
tclCOMPLETE(
tclFIRST[
tclTHEN
- (Proofview.V82.of_tactic (eapply_with_bindings (mkVar (List.nth !lid !h_num), NoBindings)))
+ (Proofview.V82.of_tactic (eapply_with_bindings (EConstr.mkVar (List.nth !lid !h_num), NoBindings)))
(Proofview.V82.of_tactic e_assumption);
Eauto.eauto_with_bases
(true,5)
- [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (Lazy.force refl_equal) sigma}]
+ [{ Tacexpr.delayed = fun _ sigma -> Sigma.here (EConstr.of_constr (Lazy.force refl_equal)) sigma}]
[Hints.Hint_db.empty empty_transparent_state false]
]
)
@@ -1366,7 +1369,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
(fun c ->
Proofview.V82.of_tactic (Tacticals.New.tclTHENLIST
[intros;
- Simple.apply (fst (interp_constr (Global.env()) Evd.empty c)) (*FIXME*);
+ Simple.apply (EConstr.of_constr (fst (interp_constr (Global.env()) Evd.empty c))) (*FIXME*);
Tacticals.New.tclCOMPLETE Auto.default_auto
])
)
@@ -1428,8 +1431,8 @@ let start_equation (f:global_reference) (term_f:global_reference)
h_intros x;
Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
observe_tac (str "simplest_case")
- (Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
- Array.of_list (List.map mkVar x)))));
+ (Proofview.V82.of_tactic (simplest_case (EConstr.of_constr (mkApp (terminate_constr,
+ Array.of_list (List.map mkVar x))))));
observe_tac (str "prove_eq") (cont_tactic x)]) g;;
let (com_eqn : int -> Id.t ->
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a943ef2b0..f96b189c5 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1461,7 +1461,7 @@ let rec make_goal_of_formula dexpr form =
xset (Term.mkNamedLetIn
(Names.Id.of_string name)
expr typ acc) l in
- xset concl l
+ EConstr.of_constr (xset concl l)
end (**
* MODULE END: M
@@ -2000,12 +2000,12 @@ let micromega_gen
(Tacticals.New.tclTHEN tac_arith tac)) in
Tacticals.New.tclTHENS
- (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+ (Tactics.forward true (Some None) (ipat_of_name goal_name) (EConstr.of_constr arith_goal))
[
kill_arith;
(Tacticals.New.tclTHENLIST
- [(Tactics.generalize (List.map Term.mkVar ids));
- Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+ [(Tactics.generalize (List.map EConstr.mkVar ids));
+ Tactics.exact_check (EConstr.of_constr (Term.applist (Term.mkVar goal_name, arith_args)))
] )
]
with
@@ -2114,12 +2114,12 @@ let micromega_genr prover tac =
(Tacticals.New.tclTHEN tac_arith tac)) in
Tacticals.New.tclTHENS
- (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+ (Tactics.forward true (Some None) (ipat_of_name goal_name) (EConstr.of_constr arith_goal))
[
kill_arith;
(Tacticals.New.tclTHENLIST
- [(Tactics.generalize (List.map Term.mkVar ids));
- Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args))
+ [(Tactics.generalize (List.map EConstr.mkVar ids));
+ Tactics.exact_check (EConstr.of_constr (Term.applist (Term.mkVar goal_name, arith_args)))
] )
]
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 36bce780b..cc0c4277e 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -625,6 +625,7 @@ let nsatz lpol =
let return_term t =
let a =
mkApp(gen_constant "CC" ["Init";"Logic"] "refl_equal",[|tllp ();t|]) in
+ let a = EConstr.of_constr a in
generalize [a]
let nsatz_compute t =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index b832250a5..35d763ccc 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -38,9 +38,9 @@ open OmegaSolver
let elim_id id =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- simplest_elim (Tacmach.New.pf_global id gl)
+ simplest_elim (EConstr.of_constr (Tacmach.New.pf_global id gl))
end }
-let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
+let resolve_id id gl = Proofview.V82.of_tactic (apply (EConstr.of_constr (pf_global gl id))) gl
let timing timer_name f arg = f arg
@@ -149,7 +149,7 @@ let mk_then = tclTHENLIST
let exists_tac c = constructor_tac false (Some 1) 1 (ImplicitBindings [c])
-let generalize_tac t = generalize t
+let generalize_tac t = generalize (List.map EConstr.of_constr t)
let elim t = simplest_elim t
let exact t = Tacmach.refine t
let unfold s = Tactics.unfold_in_concl [Locus.AllOccurrences, Lazy.force s]
@@ -373,7 +373,7 @@ let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
let mk_eq t1 t2 = mkApp (Universes.constr_of_global (build_coq_eq ()),
[| Lazy.force coq_Z; t1; t2 |])
let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
-let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
+let mk_gt t1 t2 = EConstr.of_constr (mkApp (Lazy.force coq_Zgt, [| t1; t2 |]))
let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
let mk_and t1 t2 = mkApp (build_coq_and (), [| t1; t2 |])
let mk_or t1 t2 = mkApp (build_coq_or (), [| t1; t2 |])
@@ -569,6 +569,7 @@ let abstract_path typ path t =
let focused_simpl path gl =
let newc = context (fun i t -> pf_nf gl (EConstr.of_constr t)) (List.rev path) (pf_concl gl) in
+ let newc = EConstr.of_constr newc in
Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
let focused_simpl path = focused_simpl path
@@ -1116,7 +1117,7 @@ let replay_history tactic_normalisation =
let state_eg = mk_eq eq1 rhs in
let tac = scalar_norm_add [P_APP 3] e2.body in
Tacticals.New.tclTHENS
- (cut state_eg)
+ (cut (EConstr.of_constr state_eg))
[ Tacticals.New.tclTHENS
(Tacticals.New.tclTHENLIST [
(intros_using [aux]);
@@ -1185,7 +1186,7 @@ let replay_history tactic_normalisation =
if e1.kind == DISE then
let tac = scalar_norm [P_APP 3] e2.body in
Tacticals.New.tclTHENS
- (cut state_eq)
+ (cut (EConstr.of_constr state_eq))
[Tacticals.New.tclTHENLIST [
(intros_using [aux1]);
(generalize_tac
@@ -1197,7 +1198,7 @@ let replay_history tactic_normalisation =
Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
else
let tac = scalar_norm [P_APP 3] e2.body in
- Tacticals.New.tclTHENS (cut state_eq)
+ Tacticals.New.tclTHENS (cut (EConstr.of_constr state_eq))
[
Tacticals.New.tclTHENS
(cut (mk_gt kk izero))
@@ -1227,7 +1228,7 @@ let replay_history tactic_normalisation =
scalar_norm [P_APP 3] e1.body
in
Tacticals.New.tclTHENS
- (cut (mk_eq eq1 (mk_inv eq2)))
+ (cut (EConstr.of_constr (mk_eq eq1 (mk_inv eq2))))
[Tacticals.New.tclTHENLIST [
(intros_using [aux]);
(generalize_tac [mkApp (Lazy.force coq_OMEGA8,
@@ -1260,7 +1261,7 @@ let replay_history tactic_normalisation =
shuffle_mult_right p_initial
orig.body m ({c= negone;v= v}::def.body) in
Tacticals.New.tclTHENS
- (cut theorem)
+ (cut (EConstr.of_constr theorem))
[Tacticals.New.tclTHENLIST [
(intros_using [aux]);
(elim_id aux);
@@ -1273,7 +1274,7 @@ let replay_history tactic_normalisation =
(clear [aux]);
(intros_using [id]);
(loop l) ];
- Tacticals.New.tclTHEN (exists_tac eq1) reflexivity ]
+ Tacticals.New.tclTHEN (exists_tac (EConstr.of_constr eq1)) reflexivity ]
| SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l ->
let id1 = new_identifier ()
and id2 = new_identifier () in
@@ -1283,7 +1284,7 @@ let replay_history tactic_normalisation =
let tac2 = scalar_norm_add [P_APP 2;P_TYPE] e.body in
let eq = val_of(decompile e) in
Tacticals.New.tclTHENS
- (simplest_elim (applist (Lazy.force coq_OMEGA19, [eq; mkVar id])))
+ (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_OMEGA19, [eq; mkVar id]))))
[Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac1); (intros_using [id1]); (loop act1) ];
Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (mk_then tac2); (intros_using [id2]); (loop act2) ]]
| SUM(e3,(k1,e1),(k2,e2)) :: l ->
@@ -1433,7 +1434,7 @@ let coq_omega =
let i = new_id () in
tag_hypothesis id i;
(Tacticals.New.tclTHENLIST [
- (simplest_elim (applist (Lazy.force coq_intro_Z, [t])));
+ (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_intro_Z, [t]))));
(intros_using [v; id]);
(elim_id id);
(clear [id]);
@@ -1444,7 +1445,7 @@ let coq_omega =
constant = zero; id = i} :: sys
else
(Tacticals.New.tclTHENLIST [
- (simplest_elim (applist (Lazy.force coq_new_var, [t])));
+ (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_new_var, [t]))));
(intros_using [v;th]);
tac ]),
sys)
@@ -1494,7 +1495,7 @@ let nat_inject =
let id = new_identifier () in
Tacticals.New.tclTHENS
(Tacticals.New.tclTHEN
- (simplest_elim (applist (Lazy.force coq_le_gt_dec, [t2;t1])))
+ (simplest_elim (EConstr.of_constr (applist (Lazy.force coq_le_gt_dec, [t2;t1]))))
(intros_using [id]))
[
Tacticals.New.tclTHENLIST [
@@ -1793,15 +1794,15 @@ let destructure_hyps =
| Kapp(Nat,_) ->
Tacticals.New.tclTHENLIST [
(simplest_elim
- (mkApp
- (Lazy.force coq_not_eq, [|t1;t2;mkVar i|])));
+ (EConstr.of_constr (mkApp
+ (Lazy.force coq_not_eq, [|t1;t2;mkVar i|]))));
(onClearedName i (fun _ -> loop lit))
]
| Kapp(Z,_) ->
Tacticals.New.tclTHENLIST [
(simplest_elim
- (mkApp
- (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|])));
+ (EConstr.of_constr (mkApp
+ (Lazy.force coq_not_Zeq, [|t1;t2;mkVar i|]))));
(onClearedName i (fun _ -> loop lit))
]
| _ -> loop lit
@@ -1851,7 +1852,7 @@ let destructure_goal =
(Proofview.V82.tactic (Tacmach.refine
(EConstr.of_constr (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))))
intro
- with Undecidable -> Tactics.elim_type (build_coq_False ())
+ with Undecidable -> Tactics.elim_type (EConstr.of_constr (build_coq_False ()))
in
Tacticals.New.tclTHEN goal_tac destructure_hyps
in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 7b6d502b5..2cc402e28 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -458,8 +458,8 @@ let quote f lid =
| _ -> assert false
in
match ivs.variable_lhs with
- | None -> Tactics.convert_concl (mkApp (f, [| p |])) DEFAULTcast
- | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) DEFAULTcast
+ | None -> Tactics.convert_concl (EConstr.of_constr (mkApp (f, [| p |]))) DEFAULTcast
+ | Some _ -> Tactics.convert_concl (EConstr.of_constr (mkApp (f, [| vm; p |]))) DEFAULTcast
end }
let gen_quote cont c f lid =
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index ba882e39a..ab5033601 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1222,7 +1222,7 @@ let resolution env full_reified_goal systems_list =
(* variables a introduire *)
let to_introduce = add_stated_equations env solution_tree in
let stated_vars = List.map (fun (v,_,_,_) -> v) to_introduce in
- let l_generalize_arg = List.map (fun (_,t,_,_) -> t) to_introduce in
+ let l_generalize_arg = List.map (fun (_,t,_,_) -> EConstr.of_constr t) to_introduce in
let hyp_stated_vars = List.map (fun (_,_,_,id) -> CCEqua id) to_introduce in
(* L'environnement de base se construit en deux morceaux :
- les variables des équations utiles (et de la conclusion)
@@ -1258,6 +1258,7 @@ let resolution env full_reified_goal systems_list =
let reified =
app coq_interp_sequent
[| reified_concl;env_props_reified;env_terms_reified;reified_goal|] in
+ let reified = EConstr.of_constr reified in
let normalize_equation e =
let rec loop = function
[] -> app (if e.e_negated then coq_p_invert else coq_p_step)
@@ -1281,9 +1282,9 @@ let resolution env full_reified_goal systems_list =
let decompose_tactic = decompose_tree env context solution_tree in
Proofview.V82.of_tactic (Tactics.generalize
- (l_generalize_arg @ List.map Term.mkVar (List.tl l_hyps))) >>
+ (l_generalize_arg @ List.map EConstr.mkVar (List.tl l_hyps))) >>
Proofview.V82.of_tactic (Tactics.change_concl reified) >>
- Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
+ Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (app coq_do_omega [|decompose_tactic; normalization_trace|]))) >>
show_goal >>
Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
(*i Alternatives to the previous line:
@@ -1292,7 +1293,7 @@ let resolution env full_reified_goal systems_list =
- Skip the conversion check and rely directly on the QED:
Tacmach.convert_concl_no_check (Lazy.force coq_True) Term.VMcast >>
i*)
- Proofview.V82.of_tactic (Tactics.apply (Lazy.force coq_I))
+ Proofview.V82.of_tactic (Tactics.apply (EConstr.of_constr (Lazy.force coq_I)))
let total_reflexive_omega_tactic gl =
Coqlib.check_required_library ["Coq";"romega";"ROmega"];
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index f88b3a700..981ce2a61 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -312,6 +312,7 @@ let rtauto_tac gls=
str "Giving proof term to Coq ... ")
end in
let tac_start_time = System.get_time () in
+ let term = EConstr.of_constr term in
let result=
if !check then
Proofview.V82.of_tactic (Tactics.exact_check term) gls
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index ace557a52..aa91494eb 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1392,6 +1392,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
let gl, tty = pf_type_of gl (EConstr.of_constr t) in
let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
+ let concl = EConstr.of_constr concl in
Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
(* Register "ssrpattern" tactic *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 21:44:56 +0000