From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 19:52:48 +0100 Subject: Tacmach API using EConstr. --- ltac/extratactics.ml4 | 4 +-- ltac/rewrite.ml | 2 +- plugins/btauto/refl_btauto.ml | 1 + plugins/cc/ccalgo.ml | 4 +-- plugins/cc/cctac.ml | 11 +++--- plugins/decl_mode/decl_proof_instr.ml | 14 ++++---- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/sequent.ml | 4 +-- plugins/funind/functional_principles_proofs.ml | 22 +++++++----- plugins/funind/indfun.ml | 4 +-- plugins/funind/invfun.ml | 12 +++---- plugins/funind/recdef.ml | 12 +++---- plugins/omega/coq_omega.ml | 18 +++++----- plugins/romega/const_omega.ml | 2 +- plugins/ssrmatching/ssrmatching.ml4 | 2 +- pretyping/tacred.ml | 4 +-- pretyping/tacred.mli | 6 ++-- proofs/clenvtac.ml | 2 +- proofs/logic.ml | 1 + proofs/tacmach.ml | 45 ++++++++++++----------- proofs/tacmach.mli | 50 +++++++++++++------------- tactics/class_tactics.ml | 4 +-- tactics/contradiction.ml | 2 +- tactics/eauto.ml | 2 +- tactics/elim.ml | 4 +-- tactics/eqdecide.ml | 4 +-- tactics/equality.ml | 15 ++++---- tactics/hipattern.ml | 3 +- tactics/inv.ml | 2 +- tactics/tacticals.ml | 4 +-- tactics/tactics.ml | 44 +++++++++++++++-------- toplevel/auto_ind_decl.ml | 4 +-- toplevel/command.ml | 4 +-- 33 files changed, 170 insertions(+), 144 deletions(-) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index c3ca8f906..3e7cf5d13 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -734,7 +734,7 @@ let refl_equal = call it before it is defined. *) let mkCaseEq a : unit Proofview.tactic = Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g a) gl in + let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.of_constr a)) gl in Tacticals.New.tclTHENLIST [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; Proofview.Goal.nf_enter { enter = begin fun gl -> @@ -789,7 +789,7 @@ let destauto t = let destauto_in id = Proofview.Goal.nf_enter { enter = begin fun gl -> - let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (mkVar id)) gl in + let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_unsafe_type_of g (EConstr.mkVar id)) gl in (* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) (* Pp.msgnl (Printer.pr_lconstr (ctype)); *) destauto ctype diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index dfcfbfbd3..37b9a9edb 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -2188,7 +2188,7 @@ let setoid_transitivity c = let setoid_symmetry_in id = Proofview.V82.tactic (fun gl -> - let ctype = pf_unsafe_type_of gl (mkVar id) in + let ctype = pf_unsafe_type_of gl (EConstr.mkVar id) in let binders,concl = decompose_prod_assum ctype in let (equiv, args) = decompose_app concl in let rec split_last_two = function 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 diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ae53c12ae..24d4af89a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1214,8 +1214,8 @@ let reduce_to_ind_gen allow_product env sigma t = in elimrec env t [] -let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma (EConstr.of_constr c) -let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma (EConstr.of_constr c) +let reduce_to_quantified_ind env sigma c = reduce_to_ind_gen true env sigma c +let reduce_to_atomic_ind env sigma c = reduce_to_ind_gen false env sigma c let find_hnf_rectype env sigma t = let ind,t = reduce_to_atomic_ind env sigma t in diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index d32fcf491..3587ae281 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -75,12 +75,12 @@ val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_atomic_ind : env -> evar_map -> types -> pinductive * types +val reduce_to_atomic_ind : env -> evar_map -> EConstr.types -> pinductive * types (** [reduce_to_quantified_ind env sigma t] puts [t] in the form [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_quantified_ind : env -> evar_map -> types -> pinductive * types +val reduce_to_quantified_ind : env -> evar_map -> EConstr.types -> pinductive * types (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) @@ -91,7 +91,7 @@ val reduce_to_atomic_ref : env -> evar_map -> global_reference -> EConstr.types -> types val find_hnf_rectype : - env -> evar_map -> types -> pinductive * constr list + env -> evar_map -> EConstr.types -> pinductive * constr list val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index bc5f17bf5..5b9322bfe 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -95,7 +95,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv = let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS (Evd.clear_metas evd')) - (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl + (refine_no_check (EConstr.of_constr (clenv_cast_meta clenv (clenv_value clenv)))) gl end open Unification diff --git a/proofs/logic.ml b/proofs/logic.ml index c5d6e3e08..829c96296 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -490,6 +490,7 @@ and mk_arggoals sigma goal goalacc funty allargs = and mk_casegoals sigma goal goalacc p c = let env = Goal.V82.env sigma goal in let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in + let ct = EConstr.of_constr ct in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = try Tacred.find_hnf_rectype env sigma ct diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index c2ebb76d7..b732e5b9d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -77,37 +77,36 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in let sigma = Sigma.Unsafe.of_evar_map (project gls) in - let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma (EConstr.of_constr c) in + let Sigma (c, sigma, _) = redfun.e_redfun (pf_env gls) sigma c in (Sigma.to_evar_map sigma, c) let pf_apply f gls = f (pf_env gls) (project gls) let pf_eapply f gls x = on_sig gls (fun evm -> f (pf_env gls) evm x) let pf_reduce = pf_apply -let pf_reduce' f gl c = pf_apply f gl (EConstr.of_constr c) let pf_e_reduce = pf_apply -let pf_whd_all = pf_reduce' whd_all -let pf_hnf_constr = pf_reduce' hnf_constr -let pf_nf = pf_reduce' simpl -let pf_nf_betaiota = pf_reduce' (fun _ -> nf_betaiota) -let pf_compute = pf_reduce' compute -let pf_unfoldn ubinds = pf_reduce' (unfoldn ubinds) -let pf_unsafe_type_of = pf_reduce' unsafe_type_of -let pf_type_of = pf_reduce' type_of +let pf_whd_all = pf_reduce whd_all +let pf_hnf_constr = pf_reduce hnf_constr +let pf_nf = pf_reduce simpl +let pf_nf_betaiota = pf_reduce (fun _ -> nf_betaiota) +let pf_compute = pf_reduce compute +let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) +let pf_unsafe_type_of = pf_reduce unsafe_type_of +let pf_type_of = pf_reduce type_of let pf_get_type_of = pf_reduce Retyping.get_type_of -let pf_conv_x gl = pf_apply test_conversion gl Reduction.CONV +let pf_conv_x gl = pf_reduce test_conversion gl Reduction.CONV let pf_conv_x_leq gl = pf_reduce test_conversion gl Reduction.CUMUL let pf_const_value = pf_reduce (fun env _ -> constant_value_in env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let pf_hnf_type_of gls = EConstr.of_constr %> pf_get_type_of gls %> pf_whd_all gls +let pf_hnf_type_of gls = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p (EConstr.of_constr c) -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EConstr.of_constr c) +let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c +let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c (********************************************) (* Definition of the most primitive tactics *) @@ -116,12 +115,15 @@ let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p (EC let refiner = refiner let internal_cut_no_check replace id t gl = + let t = EConstr.Unsafe.to_constr t in refiner (Cut (true,replace,id,t)) gl let internal_cut_rev_no_check replace id t gl = + let t = EConstr.Unsafe.to_constr t in refiner (Cut (false,replace,id,t)) gl let refine_no_check c gl = + let c = EConstr.Unsafe.to_constr c in refiner (Refine c) gl (* Versions with consistency checks *) @@ -159,9 +161,6 @@ module New = struct let pf_apply f gl = f (Proofview.Goal.env gl) (project gl) - let pf_reduce f gl c = - f (Proofview.Goal.env gl) (project gl) (EConstr.of_constr c) - let of_old f gl = f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; } @@ -175,10 +174,10 @@ module New = struct let pf_concl = Proofview.Goal.concl let pf_unsafe_type_of gl t = - pf_apply unsafe_type_of gl (EConstr.of_constr t) + pf_apply unsafe_type_of gl t let pf_type_of gl t = - pf_apply type_of gl (EConstr.of_constr t) + pf_apply type_of gl t let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2 @@ -221,18 +220,18 @@ module New = struct let sigma = project gl in nf_evar sigma concl - let pf_whd_all gl t = pf_reduce whd_all gl t + let pf_whd_all gl t = pf_apply whd_all gl t let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t let pf_reduce_to_quantified_ind gl t = pf_apply reduce_to_quantified_ind gl t - let pf_hnf_constr gl t = pf_reduce hnf_constr gl t + let pf_hnf_constr gl t = pf_apply hnf_constr gl t let pf_hnf_type_of gl t = - pf_whd_all gl (pf_get_type_of gl (EConstr.of_constr t)) + pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t)) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat (EConstr.of_constr t) + let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 16f6f88c1..07d02212c 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -40,9 +40,9 @@ val pf_nth_hyp_id : goal sigma -> int -> Id.t val pf_last_hyp : goal sigma -> Context.Named.Declaration.t val pf_ids_of_hyps : goal sigma -> Id.t list val pf_global : goal sigma -> Id.t -> constr -val pf_unsafe_type_of : goal sigma -> constr -> types -val pf_type_of : goal sigma -> constr -> evar_map * types -val pf_hnf_type_of : goal sigma -> constr -> types +val pf_unsafe_type_of : goal sigma -> EConstr.constr -> types +val pf_type_of : goal sigma -> EConstr.constr -> evar_map * types +val pf_hnf_type_of : goal sigma -> EConstr.constr -> types val pf_get_hyp : goal sigma -> Id.t -> Context.Named.Declaration.t val pf_get_hyp_typ : goal sigma -> Id.t -> types @@ -50,7 +50,7 @@ val pf_get_hyp_typ : goal sigma -> Id.t -> types val pf_get_new_id : Id.t -> goal sigma -> Id.t val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list -val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> evar_map * constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> EConstr.constr -> evar_map * constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a @@ -63,35 +63,35 @@ val pf_e_reduce : (env -> evar_map -> constr -> evar_map * constr) -> goal sigma -> constr -> evar_map * constr -val pf_whd_all : goal sigma -> constr -> constr -val pf_hnf_constr : goal sigma -> constr -> constr -val pf_nf : goal sigma -> constr -> constr -val pf_nf_betaiota : goal sigma -> constr -> constr -val pf_reduce_to_quantified_ind : goal sigma -> types -> pinductive * types -val pf_reduce_to_atomic_ind : goal sigma -> types -> pinductive * types -val pf_compute : goal sigma -> constr -> constr +val pf_whd_all : goal sigma -> EConstr.constr -> constr +val pf_hnf_constr : goal sigma -> EConstr.constr -> constr +val pf_nf : goal sigma -> EConstr.constr -> constr +val pf_nf_betaiota : goal sigma -> EConstr.constr -> constr +val pf_reduce_to_quantified_ind : goal sigma -> EConstr.types -> pinductive * types +val pf_reduce_to_atomic_ind : goal sigma -> EConstr.types -> pinductive * types +val pf_compute : goal sigma -> EConstr.constr -> constr val pf_unfoldn : (occurrences * evaluable_global_reference) list - -> goal sigma -> constr -> constr + -> goal sigma -> EConstr.constr -> constr val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool +val pf_matches : goal sigma -> constr_pattern -> EConstr.constr -> patvar_map +val pf_is_matching : goal sigma -> constr_pattern -> EConstr.constr -> bool (** {6 The most primitive tactics. } *) val refiner : rule -> tactic -val internal_cut_no_check : bool -> Id.t -> types -> tactic -val refine_no_check : constr -> tactic +val internal_cut_no_check : bool -> Id.t -> EConstr.types -> tactic +val refine_no_check : EConstr.constr -> tactic (** {6 The most primitive tactics with consistency and type checking } *) -val internal_cut : bool -> Id.t -> types -> tactic -val internal_cut_rev : bool -> Id.t -> types -> tactic -val refine : constr -> tactic +val internal_cut : bool -> Id.t -> EConstr.types -> tactic +val internal_cut_rev : bool -> Id.t -> EConstr.types -> tactic +val refine : EConstr.constr -> tactic (** {6 Pretty-printing functions (debug only). } *) val pr_gls : goal sigma -> Pp.std_ppcmds @@ -108,8 +108,8 @@ module New : sig val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types - val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types + val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types + val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier @@ -121,15 +121,15 @@ module New : sig val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types + val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> EConstr.types -> pinductive * types - val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types + val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types + val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> types val pf_whd_all : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr val pf_compute : ('a, 'r) Proofview.Goal.t -> EConstr.t -> constr - val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map + val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> EConstr.constr -> patvar_map val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b0f355170..a2699ba8d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -226,7 +226,7 @@ let e_give_exact flags poly (c,clenv) gl = c, {gl with sigma = evd} else c, gl in - let t1 = pf_unsafe_type_of gl c in + let t1 = pf_unsafe_type_of gl (EConstr.of_constr c) in Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) -> @@ -1514,7 +1514,7 @@ let is_ground c gl = let autoapply c i gl = let flags = auto_unif_flags Evar.Set.empty (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in - let cty = pf_unsafe_type_of gl c in + let cty = pf_unsafe_type_of gl (EConstr.of_constr c) in let ce = mk_clenv_from gl (c,cty) in let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),0,ce) } in diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 9580fdbfc..2058b95a6 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in - let typ = type_of c in + let typ = type_of (EConstr.of_constr c) in let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in if is_empty_type sigma ccl then Tacticals.New.tclTHEN diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 0869ac0c7..2fad4fcf7 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -30,7 +30,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter { enter = begin fun gl -> - let t1 = Tacmach.New.pf_unsafe_type_of gl c in + let t1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in let sigma = Tacmach.New.project gl in if occur_existential sigma (EConstr.of_constr t1) || occur_existential sigma (EConstr.of_constr t2) then diff --git a/tactics/elim.ml b/tactics/elim.ml index b830ccefe..bcb1c05cc 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -80,7 +80,7 @@ let general_decompose recognizer c = Proofview.Goal.enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let sigma = project gl in - let typc = type_of c in + let typc = type_of (EConstr.of_constr c) in tclTHENS (cut typc) [ tclTHEN (intro_using tmphyp_name) (onLastHypId @@ -133,7 +133,7 @@ let induction_trailer abs_i abs_j bargs = (onLastHypId (fun id -> Proofview.Goal.nf_enter { enter = begin fun gl -> - let idty = pf_unsafe_type_of gl (mkVar id) in + let idty = pf_unsafe_type_of gl (EConstr.mkVar id) in let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in let possible_bring_hyps = (List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 1554d43f0..d1b14a907 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -156,7 +156,7 @@ let rec solveArg hyps eqonleft op largs rargs = match largs, rargs with ] | a1 :: largs, a2 :: rargs -> Proofview.Goal.enter { enter = begin fun gl -> - let rectype = pf_unsafe_type_of gl a1 in + let rectype = pf_unsafe_type_of gl (EConstr.of_constr a1) in let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in let tac hyp = solveArg (hyp :: hyps) eqonleft op largs rargs in let subtacs = @@ -226,7 +226,7 @@ let decideEquality rectype = let compare c1 c2 = Proofview.Goal.enter { enter = begin fun gl -> - let rectype = pf_unsafe_type_of gl c1 in + let rectype = pf_unsafe_type_of gl (EConstr.of_constr c1) in let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in (tclTHENS (cut decide) [(tclTHEN intro diff --git a/tactics/equality.ml b/tactics/equality.ml index 64b56b99b..ad80d2d1f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -181,8 +181,8 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl = in List.map try_occ occs let instantiate_lemma gl c ty l l2r concl = - let sigma, ct = pf_type_of gl c in - let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma ct) with UserError _ -> ct in + let sigma, ct = pf_type_of gl (EConstr.of_constr c) in + let t = try snd (reduce_to_quantified_ind (pf_env gl) sigma (EConstr.of_constr ct)) with UserError _ -> ct in let eqclause = Clenv.make_clenv_binding (pf_env gl) sigma (c,t) l in [eqclause] @@ -992,6 +992,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in + let pf = EConstr.of_constr pf in Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS eff <*> tclTHENS (assert_after Anonymous absurd_term) @@ -1012,8 +1013,8 @@ let onEquality with_evars tac (c,lbindc) = Proofview.Goal.nf_enter { enter = begin fun gl -> let type_of = pf_unsafe_type_of gl in let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in - let t = type_of c in - let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in + let t = type_of (EConstr.of_constr c) in + let t' = try snd (reduce_to_quantified_ind (EConstr.of_constr t)) with UserError _ -> t in let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in let eqn = clenv_type eq_clause' in @@ -1327,7 +1328,7 @@ let inject_if_homogenous_dependent_pair ty = if not (Ind_tables.check_scheme (!eq_dec_scheme_kind_name()) (fst ind) && pf_apply is_conv gl (EConstr.of_constr ar1.(2)) (EConstr.of_constr ar2.(2))) then raise Exit; Coqlib.check_required_library ["Coq";"Logic";"Eqdep_dec"]; - let new_eq_args = [|pf_unsafe_type_of gl ar1.(3);ar1.(3);ar2.(3)|] in + let new_eq_args = [|pf_unsafe_type_of gl (EConstr.of_constr ar1.(3));ar1.(3);ar2.(3)|] in let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in let c, eff = find_scheme (!eq_dec_scheme_kind_name()) (Univ.out_punivs ind) in @@ -1339,7 +1340,7 @@ let inject_if_homogenous_dependent_pair ty = tclTHENS (cut (mkApp (ceq,new_eq_args))) [clear [destVar hyp]; Proofview.V82.tactic (Tacmach.refine - (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|]))) + (EConstr.of_constr (mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])))) ])] with Exit -> Proofview.tclUNIT () @@ -1384,7 +1385,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) [inject_if_homogenous_dependent_pair ty; - Proofview.V82.tactic (Tacmach.refine pf)]) + Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 87e252a38..5d78fd585 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -437,7 +437,7 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *) let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (t,e1,e2) + let t = pf_unsafe_type_of gl (EConstr.of_constr e1) in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2) @@ -463,6 +463,7 @@ let match_eq_nf gls eqn (ref, hetero) = let n = if hetero then 4 else 3 in let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in let pat = mkPattern (mkGAppRef ref args) in + let eqn = EConstr.of_constr eqn in match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); diff --git a/tactics/inv.ml b/tactics/inv.ml index eebc67222..2f5186f81 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -438,7 +438,7 @@ let raw_inversion inv_kind id status names = let concl = Proofview.Goal.concl gl in let c = mkVar id in let (ind, t) = - try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) + try pf_apply Tacred.reduce_to_atomic_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) with UserError _ -> let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in CErrors.user_err msg diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 2754db010..02909243d 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -628,7 +628,7 @@ module New = struct (Proofview.Goal.nf_enter { enter = begin fun gl -> let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in (* applying elimination_scheme just a little modified *) - let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl elim)) gl in + let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (elim,Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim))) gl in let indmv = match kind_of_term (last_arg elimclause.evd (EConstr.of_constr elimclause.templval.Evd.rebus)) with | Meta mv -> mv @@ -678,7 +678,7 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter { enter = begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 639a12b34..b9a219a2c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -457,6 +457,7 @@ let assert_before_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in + let t = EConstr.of_constr t in Tacticals.New.tclTHENLAST (Proofview.V82.tactic (fun gl -> @@ -476,6 +477,7 @@ let assert_after_then_gen b naming t tac = let open Context.Rel.Declaration in Proofview.Goal.enter { enter = begin fun gl -> let id = find_name b (LocalAssum (Anonymous,t)) naming gl in + let t = EConstr.of_constr t in Tacticals.New.tclTHENFIRST (Proofview.V82.tactic (fun gl -> @@ -1303,6 +1305,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) if not with_evars && occur_meta clenv.evd (EConstr.of_constr new_hyp_typ) then error_uninstantiated_metas new_hyp_typ clenv; let new_hyp_prf = clenv_value clenv in + let new_hyp_prf = EConstr.of_constr new_hyp_prf in let exact_tac = Proofview.V82.tactic (Tacmach.refine_no_check new_hyp_prf) in let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in @@ -1434,7 +1437,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let ct = Retyping.get_type_of env sigma (EConstr.of_constr c) in - let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in + let t = try snd (reduce_to_quantified_ind env sigma (EConstr.of_constr ct)) with UserError _ -> ct in let elimtac = elimination_clause_scheme with_evars in let indclause = make_clenv_binding env sigma (c, t) lbindc in let sigma = meta_merge sigma (clear_metas indclause.evd) in @@ -1452,6 +1455,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let t = Retyping.get_type_of env (Sigma.to_evar_map sigma) (EConstr.of_constr c) in + let t = EConstr.of_constr t in let (mind,_) = reduce_to_quantified_ind env (Sigma.to_evar_map sigma) t in let sort = Tacticals.New.elimination_sort_of_goal gl in let Sigma (elim, sigma, p) = @@ -1491,7 +1495,8 @@ let find_ind_eliminator ind s gl = evd, c let find_eliminator c gl = - let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (Tacmach.New.pf_unsafe_type_of gl c) in + let c = EConstr.of_constr c in + let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl c)) in if is_nonrec ind then raise IsNonrec; let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in evd, {elimindex = None; elimbody = (c,NoBindings); @@ -1637,6 +1642,7 @@ let descend_in_conjunctions avoid tac (err, info) c = let sigma = Tacmach.New.project gl in try let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in + let t = EConstr.of_constr t in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = decompose_prod_assum t in match match_with_tuple sigma ccl with @@ -1661,6 +1667,7 @@ let descend_in_conjunctions avoid tac (err, info) c = match make_projection env sigma params cstr sign elim i n c u with | None -> Tacticals.New.tclFAIL 0 (mt()) | Some (p,pt) -> + let p = EConstr.of_constr p in Tacticals.New.tclTHENS (assert_before_gen false (NamingAvoid avoid) pt) [Proofview.V82.tactic (refine p); @@ -1920,7 +1927,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam let cut_and_apply c = Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_unsafe_type_of gl c)) with + match kind_of_term (Tacmach.New.pf_hnf_constr gl (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c)))) with | Prod (_,c1,c2) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr c2) -> let concl = Proofview.Goal.concl gl in let env = Tacmach.New.pf_env gl in @@ -2201,6 +2208,7 @@ let constructor_tac with_evars expctdnumopt i lbind = let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in + let cl = EConstr.of_constr cl in let (mind,redcl) = reduce_to_quantified_ind cl in let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in @@ -2240,6 +2248,7 @@ let any_constructor with_evars tacopt = let reduce_to_quantified_ind = Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl in + let cl = EConstr.of_constr cl in let mind = fst (reduce_to_quantified_ind cl) in let nconstr = Array.length (snd (Global.lookup_inductive (fst mind))).mind_consnames in @@ -2298,7 +2307,8 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq loc l thin tac id = Proofview.Goal.nf_enter { enter = begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in + let t = EConstr.of_constr t in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in match my_find_eq_data_decompose gl t with | Some (eq,u,eq_args) -> @@ -2312,7 +2322,8 @@ let intro_decomp_eq loc l thin tac id = let intro_or_and_pattern loc with_evars bracketed ll thin tac id = Proofview.Goal.enter { enter = begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in + let t = EConstr.of_constr t in let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in let branchsigns = compute_constructor_signatures false ind in let nv_with_let = Array.map List.length branchsigns in @@ -2337,7 +2348,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let sigma = Tacmach.New.project gl in let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in - let t = whd_all (EConstr.of_constr (type_of (mkVar id))) in + let t = whd_all (EConstr.of_constr (type_of (EConstr.mkVar id))) in let eqtac, thin = match match_with_equality_type sigma t with | Some (hdcncl,[_;lhs;rhs]) -> if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then @@ -2747,7 +2758,7 @@ let forward b usetac ipat c = match usetac with | None -> Proofview.Goal.enter { enter = begin fun gl -> - let t = Tacmach.New.pf_unsafe_type_of gl c in + let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in let hd = head_ident c in Tacticals.New.tclTHENFIRST (assert_as true hd ipat t) (exact_no_check c) end } @@ -3233,7 +3244,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = | Var id -> id | _ -> let type_of = Tacmach.New.pf_unsafe_type_of gl in - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in let x = fresh_id_in_env avoid id env in Tacticals.New.tclTHEN (letin_tac None (Name x) c None allHypsAndConcl) @@ -3645,7 +3656,7 @@ let abstract_args gl generalize_vars dep id defined f args = let decl = List.hd rel in RelDecl.get_name decl, RelDecl.get_type decl, c in - let argty = Tacmach.pf_unsafe_type_of gl arg in + let argty = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr arg) in let sigma', ty = Evarsolve.refresh_universes (Some true) env !sigma (EConstr.of_constr ty) in let () = sigma := sigma' in let lenctx = List.length ctx in @@ -3686,7 +3697,7 @@ let abstract_args gl generalize_vars dep id defined f args = true, mkApp (f', before), after in if dogen then - let tyf' = Tacmach.pf_unsafe_type_of gl f' in + let tyf' = Tacmach.pf_unsafe_type_of gl (EConstr.of_constr f') in let arity, ctx, ctxenv, c', args, eqs, refls, nogen, vars, env = Array.fold_left aux (tyf',[],env,f',[],[],[],Id.Set.empty,Id.Set.empty,env) args' in @@ -3794,6 +3805,7 @@ let specialize_eqs id gl = let ty' = Tacred.whd_simpl env !evars (EConstr.of_constr ty') and acc' = Tacred.whd_simpl env !evars (EConstr.of_constr acc') in let ty' = Evarutil.nf_evar !evars ty' in + let ty' = EConstr.of_constr ty' in if worked then tclTHENFIRST (Tacmach.internal_cut true id ty') (Proofview.V82.of_tactic (exact_no_check ((* refresh_universes_strict *) acc'))) gl @@ -4014,6 +4026,7 @@ let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info = let guess_elim isrec dep s hyp0 gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in + let tmptyp0 = EConstr.of_constr tmptyp0 in let mind,_ = Tacmach.New.pf_reduce_to_quantified_ind gl tmptyp0 in let evd, elimc = if isrec && not (is_nonrec (fst mind)) then find_ind_eliminator (fst mind) s gl @@ -4028,12 +4041,13 @@ let guess_elim isrec dep s hyp0 gl = let Sigma (ind, sigma, _) = build_case_analysis_scheme_default env sigma mind s in (Sigma.to_evar_map sigma, ind) in - let elimt = Tacmach.New.pf_unsafe_type_of gl elimc in + let elimt = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elimc) in evd, ((elimc, NoBindings), elimt), mkIndU mind let given_elim hyp0 (elimc,lbind as e) gl = let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in + let elimc = EConstr.of_constr elimc in Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess type scheme_signature = @@ -4069,7 +4083,7 @@ let get_elim_signature elim hyp0 gl = compute_elim_signature (given_elim hyp0 elim gl) hyp0 let is_functional_induction elimc gl = - let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (fst elimc)) in + let scheme = compute_elim_sig ~elimc (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr (fst elimc))) in (* The test is not safe: with non-functional induction on non-standard induction scheme, this may fail *) Option.is_empty scheme.indarg @@ -4466,7 +4480,7 @@ let induction_gen_l isrec with_evars elim names lc = let type_of = Tacmach.New.pf_unsafe_type_of gl in let sigma = Tacmach.New.project gl in let x = - id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in + id_of_name_using_hdchar (Global.env()) (type_of (EConstr.of_constr c)) Anonymous in let id = new_fresh_id [] x gl in let newl' = List.map (fun r -> replace_term sigma (EConstr.of_constr c) (EConstr.mkVar id) (EConstr.of_constr r)) l' in @@ -4606,6 +4620,7 @@ let elim_scheme_type elim t = let elim_type t = Proofview.Goal.s_enter { s_enter = begin fun gl -> + let t = EConstr.of_constr t in let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in Sigma.Unsafe.of_pair (elim_scheme_type elimc t, evd) @@ -4613,6 +4628,7 @@ let elim_type t = let case_type t = Proofview.Goal.s_enter { s_enter = begin fun gl -> + let t = EConstr.of_constr t in let sigma = Proofview.Goal.sigma gl in let env = Tacmach.New.pf_env gl in let (ind,t) = reduce_to_atomic_ind env (Sigma.to_evar_map sigma) t in @@ -4717,7 +4733,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter { enter = begin fun gl -> - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in + let ctype = Tacmach.New.pf_unsafe_type_of gl (EConstr.mkVar id) in let sign,t = decompose_prod_assum ctype in Proofview.tclORELSE begin diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 02c43aec5..6561627f6 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -363,7 +363,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = ) in Proofview.Goal.nf_enter { enter = begin fun gl -> - let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl p) gl in + let type_of_pq = Tacmach.New.of_old (fun gl -> pf_unsafe_type_of gl (EConstr.of_constr p)) gl in let u,v = destruct_ind type_of_pq in let lb_type_of_p = try @@ -425,7 +425,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = match (l1,l2) with | (t1::q1,t2::q2) -> Proofview.Goal.enter { enter = begin fun gl -> - let tt1 = Tacmach.New.pf_unsafe_type_of gl t1 in + let tt1 = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr t1) in if eq_constr t1 t2 then aux q1 q2 else ( let u,v = try destruct_ind tt1 diff --git a/toplevel/command.ml b/toplevel/command.ml index dbf256ba8..80f3b26e4 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1164,7 +1164,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac @@ -1201,7 +1201,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n List.map3 (fun id t (len,imps,_) -> ((id,pl),(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = - Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) + Some (List.map (Option.cata (EConstr.of_constr %> Tacmach.refine_no_check) Tacticals.tclIDTAC) fixdefs) in let init_tac = Option.map (List.map Proofview.V82.tactic) init_tac -- cgit v1.2.3