aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml1
-rw-r--r--plugins/cc/ccalgo.ml4
-rw-r--r--plugins/cc/cctac.ml11
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml14
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml22
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/invfun.ml12
-rw-r--r--plugins/funind/recdef.ml12
-rw-r--r--plugins/omega/coq_omega.ml18
-rw-r--r--plugins/romega/const_omega.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
13 files changed, 58 insertions, 50 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 3ba5da149..1e49d8cad 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -179,6 +179,7 @@ module Btauto = struct
let print_counterexample p env gl =
let var = lapp witness [|p|] in
+ let var = EConstr.of_constr var in
(* Compute an assignment that dissatisfies the goal *)
let _, var = Tacmach.pf_reduction_of_red_expr gl (Genredexpr.CbvVm None) var in
let rec to_list l = match decomp_term (Tacmach.project gl) l with
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index bc53b113d..102efe55b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -508,7 +508,7 @@ let rec add_term state t=
Not_found ->
let b=next uf in
let trm = constr_of_term t in
- let typ = pf_unsafe_type_of state.gls trm in
+ let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
let typ = canonize_name typ in
let new_node=
match t with
@@ -832,7 +832,7 @@ let complete_one_class state i=
let id = new_state_var etyp state in
app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
let _c = pf_unsafe_type_of state.gls
- (constr_of_term (term state.uf pac.cnode)) in
+ (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
let _args =
List.map (fun i -> constr_of_term (term state.uf i))
pac.args in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 11da923e1..7c78f3a17 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -243,7 +243,8 @@ let app_global f args k =
let new_app_global f args k =
Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args)))
-let new_refine c = Proofview.V82.tactic (refine c)
+let new_refine c = Proofview.V82.tactic (refine (EConstr.of_constr c))
+let refine c = refine (EConstr.of_constr c)
let assert_before n c =
Proofview.Goal.enter { enter = begin fun gl ->
@@ -265,7 +266,7 @@ let refresh_universes ty k =
let rec proof_tac p : unit Proofview.tactic =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let type_of t = Tacmach.New.pf_unsafe_type_of gl t in
+ 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
@@ -336,7 +337,7 @@ let refute_tac c t1 t2 p =
let neweq= new_app_global _eq [|intype;tt1;tt2|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name hid)))
[proof_tac p; simplest_elim false_t]
- in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k
+ in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt1)) k
end }
let refine_exact_check c gl =
@@ -354,7 +355,7 @@ let convert_to_goal_tac c t1 t2 p =
let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
[proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]
- in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k
+ in refresh_universes (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr tt2)) k
end }
let convert_to_hyp_tac c1 t1 c2 t2 p =
@@ -376,7 +377,7 @@ let discriminate_tac (cstr,u as cstru) p =
let identity = Universes.constr_of_global (Lazy.force _I) in
let trivial = Universes.constr_of_global (Lazy.force _True) in
let evm = Tacmach.New.project gl in
- let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
+ let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1))) in
let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
let outtype = mkSort outtype in
let pred = mkLambda(Name xid,outtype,mkRel 1) in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 3bb6f1b5d..031a6253a 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -491,7 +491,7 @@ let thus_tac c ctyp submetas gls =
Proofview.V82.of_tactic (exact_check proof) gls
else
let refiner = concl_refiner list proof gls in
- Tacmach.refine refiner gls
+ Tacmach.refine (EConstr.of_constr refiner) gls
(* general forward step *)
@@ -799,7 +799,7 @@ let rec take_tac wits gls =
match wits with
[] -> tclIDTAC gls
| wit::rest ->
- let typ = pf_unsafe_type_of gls wit in
+ let typ = pf_unsafe_type_of gls (EConstr.of_constr wit) in
tclTHEN (thus_tac wit typ []) (take_tac rest) gls
@@ -879,7 +879,7 @@ let start_tree env ind rp =
let build_per_info etype casee gls =
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_unsafe_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
let is_dep = dependent (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl) in
let hd,args = decompose_app (special_whd gls ctyp) in
let (ind,u) =
@@ -894,7 +894,7 @@ let build_per_info etype casee gls =
| _ -> mind.mind_nparams,None in
let params,real_args = List.chop nparams args in
let abstract_obj c body =
- let typ=pf_unsafe_type_of gls c in
+ let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
let pred= List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
@@ -1256,13 +1256,13 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
let nparams = mind.mind_nparams in
let concl=pf_concl gls in
let env=pf_env gls in
- let ctyp=pf_unsafe_type_of gls casee in
+ let ctyp=pf_unsafe_type_of gls (EConstr.of_constr casee) in
let hd,all_args = decompose_app (special_whd gls ctyp) in
let ind', u = destInd hd in
let _ = assert (eq_ind ind' ind) in (* just in case *)
let params,real_args = List.chop nparams all_args in
let abstract_obj c body =
- let typ=pf_unsafe_type_of gls c in
+ let typ=pf_unsafe_type_of gls (EConstr.of_constr c) in
lambda_create env (typ,subst_term (project gls) (EConstr.of_constr c) (EConstr.of_constr body)) in
let elim_pred = List.fold_right abstract_obj
real_args (lambda_create env (ctyp,subst_term (project gls) (EConstr.of_constr casee) (EConstr.of_constr concl))) in
@@ -1314,7 +1314,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
execute_cases fix_name per_info tacnext
p_args objs nhrec tree] gls0 in
tclTHENSV
- (refine case_term)
+ (refine (EConstr.of_constr case_term))
(Array.mapi branch_tac br) gls
| Split_patt (_, _, _) , [] ->
anomaly ~label:"execute_cases " (Pp.str "Nothing to split")
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 44bdb585a..6c245063c 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
let evmap=Refiner.project gl in
let var_id=
if id==dummy_id then dummy_bvid else
- let typ=pf_unsafe_type_of gl idc in
+ let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
(* since we know we will get a product,
reduction is not too expensive *)
let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1248b60a7..87e7192d7 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
let l = expand_constructor_hints l in
let f gr (seq,gl) =
let gl, c = pf_eapply Evd.fresh_global gl gr in
- let typ=(pf_unsafe_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
@@ -215,7 +215,7 @@ let extend_with_auto_hints l seq gl=
let (c, _, _) = c in
(try
let gr = global_of_constr c in
- let typ=(pf_unsafe_type_of gl c) in
+ let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 83fc48623..b674f40e9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -202,6 +202,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
(List.map mkVar context_hyps)
in
let to_refine = applist(mkVar h_id,List.rev context_hyps') in
+ let to_refine = EConstr.of_constr to_refine in
refine to_refine g
)
]
@@ -329,7 +330,8 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type =
let all_ids = pf_ids_of_hyps g in
let new_ids,_ = list_chop ctxt_size all_ids in
let to_refine = applist(witness_fun,List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.type_of g (EConstr.of_constr to_refine) in
+ let to_refine = EConstr.of_constr to_refine in
+ let evm, _ = pf_apply Typing.type_of g to_refine in
tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g
)
in
@@ -448,6 +450,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
List.rev_map mkVar (rec_pte_id::context_hyps_ids)
)
in
+ let to_refine = EConstr.of_constr to_refine in
(* observe_tac "rec hyp " *)
(tclTHENS
(Proofview.V82.of_tactic (assert_before (Name rec_pte_id) t_x))
@@ -497,6 +500,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
List.rev (coq_I::List.map mkVar context_hyps)
)
in
+ let to_refine = (EConstr.of_constr to_refine) in
refine to_refine g
)
]
@@ -594,7 +598,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
- let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
+ let new_term_value_eq = pf_unsafe_type_of g' (EConstr.mkVar heq_id) in
(* compute the new value of the body *)
let new_term_value =
match kind_of_term new_term_value_eq with
@@ -605,13 +609,14 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
);
anomaly (Pp.str "cannot compute new term value")
in
+ let term = EConstr.of_constr term in
let fun_body =
mkLambda(Anonymous,
pf_unsafe_type_of g' term,
- Termops.replace_term (project g') (EConstr.of_constr term) (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
+ Termops.replace_term (project g') term (EConstr.mkRel 1) (EConstr.of_constr dyn_infos.info)
)
in
- let new_body = pf_nf_betaiota g' (mkApp(fun_body,[| new_term_value |])) in
+ let new_body = pf_nf_betaiota g' (EConstr.of_constr (mkApp(fun_body,[| new_term_value |]))) in
let new_infos =
{dyn_infos with
info = new_body;
@@ -700,7 +705,7 @@ let build_proof
let dyn_infos = {dyn_info' with info =
mkCase(ci,ct,t,cb)} in
let g_nb_prod = nb_prod (project g) (EConstr.of_constr (pf_concl g)) in
- let type_of_term = pf_unsafe_type_of g t in
+ let type_of_term = pf_unsafe_type_of g (EConstr.of_constr t) in
let term_eq =
make_refl_eq (Lazy.force refl_equal) type_of_term t
in
@@ -741,7 +746,7 @@ let build_proof
let id = pf_last_hyp g' |> get_id in
let new_term =
pf_nf_betaiota g'
- (mkApp(dyn_infos.info,[|mkVar id|]))
+ (EConstr.of_constr (mkApp(dyn_infos.info,[|mkVar id|])))
in
let new_infos = {dyn_infos with info = new_term} in
let do_prove new_hyps =
@@ -908,6 +913,7 @@ let prove_rec_hyp_for_struct fix_info =
let rec_hyp_proof =
mkApp(mkVar fix_info.name,array_get_start pte_args)
in
+ let rec_hyp_proof = EConstr.of_constr rec_hyp_proof in
refine rec_hyp_proof g
))
@@ -921,7 +927,7 @@ let generalize_non_dep hyp g =
(* observe (str "rec id := " ++ Ppconstr.pr_id hyp); *)
let hyps = [hyp] in
let env = Global.env () in
- let hyp_typ = pf_unsafe_type_of g (mkVar hyp) in
+ let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hyp) in
let to_revert,_ =
let open Context.Named.Declaration in
Environ.fold_named_context_reverse (fun (clear,keep) decl ->
@@ -1418,7 +1424,7 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
let rewrite =
tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
in
- let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (mkVar hrec)) in
+ let _,hrec_concl = decompose_prod (pf_unsafe_type_of gls (EConstr.mkVar hrec)) in
let f_app = Array.last (snd (destApp hrec_concl)) in
let f = (fst (destApp f_app)) in
let rec backtrack : tactic =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0743fc5d9..e3ba52246 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -75,11 +75,11 @@ let functional_induction with_clean c princl pat =
user_err (str "Cannot find induction principle for "
++Printer.pr_lconstr (mkConst c') )
in
- (princ,NoBindings, Tacmach.pf_unsafe_type_of g' princ,g')
+ (princ,NoBindings, Tacmach.pf_unsafe_type_of g' (EConstr.of_constr princ),g')
| _ -> raise (UserError(None,str "functional induction must be used with a function" ))
end
| Some ((princ,binding)) ->
- princ,binding,Tacmach.pf_unsafe_type_of g princ,g
+ 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 args_as_induction_constr =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e5286fb1f..635925562 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -305,7 +305,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
let constructor_args g =
List.fold_right
(fun hid acc ->
- let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+ let type_of_hid = pf_unsafe_type_of g (EConstr.mkVar hid) in
match kind_of_term type_of_hid with
| Prod(_,_,t') ->
begin
@@ -596,7 +596,7 @@ let rec reflexivity_with_destruct_cases g =
match sc with
None -> tclIDTAC g
| Some id ->
- match kind_of_term (pf_unsafe_type_of g (mkVar id)) with
+ match kind_of_term (pf_unsafe_type_of g (EConstr.mkVar id)) with
| App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
if Equality.discriminable (pf_env g) (project g) t1 t2
then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -661,7 +661,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
(* We get the constant and the principle corresponding to this lemma *)
let f = funcs.(i) in
let graph_principle = nf_zeta (EConstr.of_constr schemes.(i)) in
- let princ_type = pf_unsafe_type_of g graph_principle 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
(* Then we get the number of argument of the function
and compute a fresh name for each of them
@@ -919,7 +919,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
*)
let revert_graph kn post_tac hid g =
- let typ = pf_unsafe_type_of g (mkVar hid) in
+ let typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
match kind_of_term typ with
| App(i,args) when isInd i ->
let ((kn',num) as ind'),u = destInd i in
@@ -970,7 +970,7 @@ let revert_graph kn post_tac hid g =
let functional_inversion kn hid fconst f_correct : tactic =
fun g ->
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 (mkVar hid) 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 ()) ->
let pre_tac,f_args,res =
@@ -1022,7 +1022,7 @@ let invfun qhyp f g =
Proofview.V82.of_tactic begin
Tactics.try_intros_until
(fun hid -> Proofview.V82.tactic begin fun g ->
- let hyp_typ = pf_unsafe_type_of g (mkVar hid) in
+ 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 ()) ->
begin
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bdbf0242d..b2c93a754 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -117,7 +117,7 @@ let pf_get_new_ids idl g =
let compute_renamed_type gls c =
rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
- (pf_unsafe_type_of gls c)
+ (pf_unsafe_type_of gls (EConstr.of_constr c))
let h'_id = Id.of_string "h'"
let teq_id = Id.of_string "teq"
let ano_id = Id.of_string "anonymous"
@@ -402,7 +402,7 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
Proofview.V82.of_tactic (clear to_intros);
h_intros to_intros;
(fun g' ->
- let ty_teq = pf_unsafe_type_of g' (mkVar heq) in
+ let ty_teq = pf_unsafe_type_of g' (EConstr.mkVar heq) in
let teq_lhs,teq_rhs =
let _,args = try destApp ty_teq with DestKO -> assert false in
args.(1),args.(2)
@@ -516,13 +516,13 @@ let rec prove_lt hyple g =
in
let h =
List.find (fun id ->
- match decompose_app (pf_unsafe_type_of g (mkVar id)) with
+ match decompose_app (pf_unsafe_type_of g (EConstr.mkVar id)) with
| _, t::_ -> eq_constr t varx
| _ -> false
) hyple
in
let y =
- List.hd (List.tl (snd (decompose_app (pf_unsafe_type_of g (mkVar h))))) in
+ 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|])));
observe_tac (str "prove_lt") (prove_lt hyple)
@@ -684,7 +684,7 @@ let mkDestructEq :
if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) (EConstr.of_constr expr) (EConstr.of_constr (get_type decl)))
then None else Some id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
- let type_of_expr = pf_unsafe_type_of g expr in
+ 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
pf_typel new_hyps (fun _ ->
@@ -839,7 +839,7 @@ let rec prove_le g =
let matching_fun =
pf_is_matching g
(Pattern.PApp(Pattern.PRef (reference_of_constr (le ())),[|Pattern.PVar (destVar x);Pattern.PMeta None|])) in
- let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
+ let (h,t) = List.find (fun (_,t) -> matching_fun (EConstr.of_constr t)) (pf_hyps_types g)
in
let y =
let _,args = decompose_app t in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index d15449aef..b832250a5 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -568,7 +568,7 @@ let abstract_path typ path t =
mkLambda (Name (Id.of_string "x"), typ, abstract), !term_occur
let focused_simpl path gl =
- let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
+ let newc = context (fun i t -> pf_nf gl (EConstr.of_constr t)) (List.rev path) (pf_concl gl) in
Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl
let focused_simpl path = focused_simpl path
@@ -644,7 +644,7 @@ let clever_rewrite_base_poly typ p result theorem gl =
[| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
[abstracted])
in
- exact (applist(t,[mkNewMeta()])) gl
+ exact (EConstr.of_constr (applist(t,[mkNewMeta()]))) gl
let clever_rewrite_base p result theorem gl =
clever_rewrite_base_poly (Lazy.force coq_Z) p result theorem gl
@@ -665,7 +665,7 @@ let clever_rewrite p vpath t gl =
let (abstracted,occ) = abstract_path (Lazy.force coq_Z) (List.rev p) full in
let vargs = List.map (fun p -> occurrence p occ) vpath in
let t' = applist(t, (vargs @ [abstracted])) in
- exact (applist(t',[mkNewMeta()])) gl
+ exact (EConstr.of_constr (applist(t',[mkNewMeta()]))) gl
let rec shuffle p (t1,t2) =
match t1,t2 with
@@ -1384,7 +1384,7 @@ let destructure_omega gl tac_def (id,c) =
else
try match destructurate_prop c with
| Kapp(Eq,[typ;t1;t2])
- when begin match destructurate_type (pf_nf gl typ) with Kapp(Z,[]) -> true | _ -> false end ->
+ when begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with Kapp(Z,[]) -> true | _ -> false end ->
let t = mk_plus t1 (mk_inv t2) in
normalize_equation
id EQUA (Lazy.force coq_Zegal_left) 2 t t1 t2 tac_def
@@ -1659,7 +1659,7 @@ let rec decidability gl t =
| Kapp(Not,[t1]) ->
mkApp (Lazy.force coq_dec_not, [| t1; decidability gl t1 |])
| Kapp(Eq,[typ;t1;t2]) ->
- begin match destructurate_type (pf_nf gl typ) with
+ begin match destructurate_type (pf_nf gl (EConstr.of_constr typ)) with
| Kapp(Z,[]) -> mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
| Kapp(Nat,[]) -> mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
| _ -> raise Undecidable
@@ -1720,7 +1720,7 @@ let destructure_hyps =
| Kimp(t1,t2) ->
(* t1 and t2 might be in Type rather than Prop.
For t1, the decidability check will ensure being Prop. *)
- if is_Prop (type_of t2)
+ if is_Prop (type_of (EConstr.of_constr t2))
then
let d1 = decidability t1 in
Tacticals.New.tclTHENLIST [
@@ -1789,7 +1789,7 @@ let destructure_hyps =
with Not_found -> loop lit)
| Kapp(Eq,[typ;t1;t2]) ->
if !old_style_flag then begin
- match destructurate_type (pf_nf typ) with
+ match destructurate_type (pf_nf (EConstr.of_constr typ)) with
| Kapp(Nat,_) ->
Tacticals.New.tclTHENLIST [
(simplest_elim
@@ -1806,7 +1806,7 @@ let destructure_hyps =
]
| _ -> loop lit
end else begin
- match destructurate_type (pf_nf typ) with
+ match destructurate_type (pf_nf (EConstr.of_constr typ)) with
| Kapp(Nat,_) ->
(Tacticals.New.tclTHEN
(convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|]))
@@ -1849,7 +1849,7 @@ let destructure_goal =
let dec = decidability t in
Tacticals.New.tclTHEN
(Proofview.V82.tactic (Tacmach.refine
- (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |]))))
+ (EConstr.of_constr (mkApp (Lazy.force coq_dec_not_not, [| t; dec; mkNewMeta () |])))))
intro
with Undecidable -> Tactics.elim_type (build_coq_False ())
in
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 4935fe4bb..f2d91bad3 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -353,7 +353,7 @@ let parse_term t =
let parse_rel gl t =
try match destructurate t with
| Kapp("eq",[typ;t1;t2])
- when destructurate (Tacmach.pf_nf gl typ) = Kapp("Z",[]) -> Req (t1,t2)
+ when destructurate (Tacmach.pf_nf gl (EConstr.of_constr typ)) = Kapp("Z",[]) -> Req (t1,t2)
| Kapp("Zne",[t1;t2]) -> Rne (t1,t2)
| Kapp("Z.le",[t1;t2]) -> Rle (t1,t2)
| Kapp("Z.lt",[t1;t2]) -> Rlt (t1,t2)
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7f628f165..ace557a52 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1390,7 +1390,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
let concl0 = pf_concl gl in
let (t, uc), concl_x =
fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
- let gl, tty = pf_type_of gl t 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
Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 19:01:55 +0000