From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 13 Nov 2016 20:38:41 +0100 Subject: Tactics API using EConstr. --- ltac/coretactics.ml4 | 20 ++++++++++---------- ltac/extratactics.ml4 | 23 +++++++++++++---------- ltac/g_auto.ml4 | 12 ++++++++---- ltac/g_rewrite.ml4 | 2 +- ltac/pptactic.ml | 17 +++++++++-------- ltac/rewrite.ml | 35 ++++++++++++++++++++--------------- ltac/rewrite.mli | 2 +- ltac/tacexpr.mli | 6 +++--- ltac/tacinterp.ml | 29 ++++++++++++++++++++++------- ltac/tauto.ml | 10 ++++++---- 10 files changed, 93 insertions(+), 63 deletions(-) (limited to 'ltac') diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index 28ff6df838..20d9640fc4 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -27,7 +27,7 @@ TACTIC EXTEND reflexivity END TACTIC EXTEND exact - [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ] + [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ] END TACTIC EXTEND assumption @@ -39,35 +39,35 @@ TACTIC EXTEND etransitivity END TACTIC EXTEND cut - [ "cut" constr(c) ] -> [ Tactics.cut c ] + [ "cut" constr(c) ] -> [ Tactics.cut (EConstr.of_constr c) ] END TACTIC EXTEND exact_no_check - [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ] + [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ] END TACTIC EXTEND vm_cast_no_check - [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ] + [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check (EConstr.of_constr c) ] END TACTIC EXTEND native_cast_no_check - [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ] + [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check (EConstr.of_constr c) ] END TACTIC EXTEND casetype - [ "casetype" constr(c) ] -> [ Tactics.case_type c ] + [ "casetype" constr(c) ] -> [ Tactics.case_type (EConstr.of_constr c) ] END TACTIC EXTEND elimtype - [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ] + [ "elimtype" constr(c) ] -> [ Tactics.elim_type (EConstr.of_constr c) ] END TACTIC EXTEND lapply - [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] + [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply (EConstr.of_constr c) ] END TACTIC EXTEND transitivity - [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] + [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some (EConstr.of_constr c)) ] END (** Left *) @@ -297,7 +297,7 @@ END (* Generalize dependent *) TACTIC EXTEND generalize_dependent - [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ] + [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep (EConstr.of_constr c) ] END (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 3e7cf5d13b..c39b1a0e94 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -118,7 +118,7 @@ END let discrHyp id = Proofview.tclEVARMAP >>= fun sigma -> - discr_main { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } + discr_main { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } let injection_main with_evars c = elimOnConstrWithHoles (injClause None) with_evars c @@ -150,7 +150,7 @@ END let injHyp id = Proofview.tclEVARMAP >>= fun sigma -> - injection_main false { delayed = fun env sigma -> Sigma.here (Term.mkVar id, NoBindings) sigma } + injection_main false { delayed = fun env sigma -> Sigma.here (EConstr.mkVar id, NoBindings) sigma } TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -301,6 +301,7 @@ let project_hint pri l2r r = let t = Retyping.get_type_of env sigma (EConstr.of_constr c) in let t = Tacred.reduce_to_quantified_ref env sigma (Lazy.force coq_iff_ref) (EConstr.of_constr t) in + let t = EConstr.Unsafe.to_constr t in let sign,ccl = decompose_prod_assum t in let (a,b) = match snd (decompose_app ccl) with | [a;b] -> (a,b) @@ -475,6 +476,7 @@ let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" let step left x tac = let l = List.map (fun lem -> + let lem = EConstr.of_constr lem in Tacticals.New.tclTHENLAST (apply_with_bindings (lem, ImplicitBindings [x])) tac) @@ -510,13 +512,13 @@ let add_transitivity_lemma left lem = (* Vernacular syntax *) TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ] -| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] +| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ] +| ["stepl" constr(c) ] -> [ step true (EConstr.of_constr c) (Proofview.tclUNIT ()) ] END TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ] -| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] +| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false (EConstr.of_constr c) (Tacinterp.tactic_of_value ist tac) ] +| ["stepr" constr(c) ] -> [ step false (EConstr.of_constr c) (Proofview.tclUNIT ()) ] END VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF @@ -660,7 +662,7 @@ let hResolve id c occ t = let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma (EConstr.of_constr t_constr) in let tac = - (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) + (change_concl (EConstr.of_constr (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))) in Sigma.Unsafe.of_pair (tac, sigma) end } @@ -694,7 +696,7 @@ let hget_evar n = if n <= 0 then error "Incorrect existential variable index."; let ev = List.nth evl (n-1) in let ev_type = existential_type sigma ev in - change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) + change_concl (EConstr.of_constr (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))) end } TACTIC EXTEND hget_evar @@ -736,15 +738,16 @@ 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 (EConstr.of_constr a)) gl in Tacticals.New.tclTHENLIST - [Tactics.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]; + [Tactics.generalize [EConstr.of_constr (mkApp(delayed_force refl_equal, [| type_of_a; a|]))]; Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in (** FIXME: this looks really wrong. Does anybody really use this tactic? *) let Sigma (c, _, _) = (Tacred.pattern_occs [Locus.OnlyOccurrences [1], EConstr.of_constr a]).Reductionops.e_redfun env (Sigma.Unsafe.of_evar_map Evd.empty) (EConstr.of_constr concl) in + let c = EConstr.of_constr c in change_concl c end }; - simplest_case a] + simplest_case (EConstr.of_constr a)] end } diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 82ba63871e..c6395d7e28 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -48,7 +48,11 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs + let map c = { delayed = fun env sigma -> + let Sigma.Sigma (c, sigma, p) = c.delayed env sigma in + Sigma.Sigma (EConstr.of_constr c, sigma, p) + } in + List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) @@ -153,7 +157,7 @@ TACTIC EXTEND autounfoldify END TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] +| ["unify" constr(x) constr(y) ] -> [ Tactics.unify (EConstr.of_constr x) (EConstr.of_constr y) ] | ["unify" constr(x) constr(y) "with" preident(base) ] -> [ let table = try Some (Hints.searchtable_map base) with Not_found -> None in match table with @@ -162,13 +166,13 @@ TACTIC EXTEND unify Tacticals.New.tclZEROMSG msg | Some t -> let state = Hints.Hint_db.transparent_state t in - Tactics.unify ~state x y + Tactics.unify ~state (EConstr.of_constr x) (EConstr.of_constr y) ] END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ] +| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check (EConstr.of_constr x) Term.DEFAULTcast ] END let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4 index b1c4f58eb8..bae5a516c7 100644 --- a/ltac/g_rewrite.ml4 +++ b/ltac/g_rewrite.ml4 @@ -265,7 +265,7 @@ TACTIC EXTEND setoid_reflexivity END TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] + [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some (EConstr.of_constr t)) ] | [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] END diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index 6230fa0606..934830f4db 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -1158,11 +1158,12 @@ module Make let pr_glob_tactic env = pr_glob_tactic_level env ltop let strip_prod_binders_constr n ty = + let ty = EConstr.Unsafe.to_constr ty in let rec strip_ty acc n ty = - if n=0 then (List.rev acc, ty) else + if n=0 then (List.rev acc, EConstr.of_constr ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([Loc.ghost,na],a)::acc) (n-1) b + strip_ty (([Loc.ghost,na],EConstr.of_constr a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1170,9 +1171,9 @@ module Make let prtac n (t:atomic_tactic_expr) = let pr = { pr_tactic = (fun _ _ -> str ""); - pr_constr = pr_constr_env env Evd.empty; + pr_constr = (fun c -> pr_constr_env env Evd.empty (EConstr.Unsafe.to_constr c)); pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env); - pr_lconstr = pr_lconstr_env env Evd.empty; + pr_lconstr = (fun c -> pr_lconstr_env env Evd.empty (EConstr.Unsafe.to_constr c)); pr_pattern = pr_constr_pattern_env env Evd.empty; pr_lpattern = pr_lconstr_pattern_env env Evd.empty; pr_constant = pr_evaluable_reference_env env; @@ -1284,7 +1285,7 @@ let () = wit_intro_pattern (Miscprint.pr_intro_pattern pr_constr_expr) (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr c)) - (Miscprint.pr_intro_pattern (fun c -> pr_constr (fst (run_delayed c)))); + (Miscprint.pr_intro_pattern (fun c -> pr_constr (EConstr.Unsafe.to_constr (fst (run_delayed c))))); Genprint.register_print0 wit_clause_dft_concl (pr_clauses (Some true) pr_lident) @@ -1317,15 +1318,15 @@ let () = Genprint.register_print0 wit_bindings (pr_bindings_no_with pr_constr_expr pr_lconstr_expr) (pr_bindings_no_with (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_bindings_no_with pr_constr pr_lconstr (fst (run_delayed it))); + (fun it -> pr_bindings_no_with (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it))); Genprint.register_print0 wit_constr_with_bindings (pr_with_bindings pr_constr_expr pr_lconstr_expr) (pr_with_bindings (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_with_bindings pr_constr pr_lconstr (fst (run_delayed it))); + (fun it -> pr_with_bindings (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it))); Genprint.register_print0 Tacarg.wit_destruction_arg (pr_destruction_arg pr_constr_expr pr_lconstr_expr) (pr_destruction_arg (pr_and_constr_expr pr_glob_constr) (pr_and_constr_expr pr_lglob_constr)) - (fun it -> pr_destruction_arg pr_constr pr_lconstr (run_delayed_destruction_arg it)); + (fun it -> pr_destruction_arg (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (run_delayed_destruction_arg it)); Genprint.register_print0 Stdarg.wit_int int int int; Genprint.register_print0 Stdarg.wit_bool pr_bool pr_bool pr_bool; Genprint.register_print0 Stdarg.wit_unit pr_unit pr_unit pr_unit; diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 52cf1ff357..ef2ab09176 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -97,8 +97,8 @@ let new_cstr_evar (evd,cstrs) env t = let evd = Sigma.Unsafe.of_evar_map evd in let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd (EConstr.of_constr t) in let evd' = Sigma.to_evar_map evd' in - let ev, _ = destEvar t in - (evd', Evar.Set.add ev cstrs), t + let ev, _ = EConstr.destEvar evd' t in + (evd', Evar.Set.add ev cstrs), EConstr.Unsafe.to_constr t (** Building or looking up instances. *) let e_new_cstr_evar env evars t = @@ -363,6 +363,7 @@ end) = struct let env' = Environ.push_rel_context rels env in let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in + let evar = EConstr.Unsafe.to_constr evar in let evars = Sigma.to_evar_map evars in let evars, inst = app_poly env (evars,Evar.Set.empty) @@ -774,7 +775,7 @@ let poly_subrelation sort = if sort then PropGlobal.subrelation else TypeGlobal.subrelation let resolve_subrelation env avoid car rel sort prf rel' res = - if eq_constr rel rel' then res + if Termops.eq_constr (fst res.rew_evars) (EConstr.of_constr rel) (EConstr.of_constr rel') then res else let evars, app = app_poly_check env res.rew_evars (poly_subrelation sort) [|car; rel; rel'|] in let evars, subrel = new_cstr_evar evars env app in @@ -872,7 +873,7 @@ let apply_rule unify loccs : int pure_strategy = | Some rew -> let occ = succ occ in if not (is_occ occ) then (occ, Fail) - else if eq_constr t rew.rew_to then (occ, Identity) + else if Termops.eq_constr (fst rew.rew_evars) (EConstr.of_constr t) (EConstr.of_constr rew.rew_to) then (occ, Identity) else let res = { rew with rew_car = ty } in let rel, prf = get_rew_prf res in @@ -1111,7 +1112,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = | Prod (n, dom, codom) -> let lam = mkLambda (n, dom, codom) in let (evars', app), unfold = - if eq_constr ty mkProp then + if eq_constr (fst evars) (EConstr.of_constr ty) EConstr.mkProp then (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all else let forall = if prop then PropGlobal.coq_forall else TypeGlobal.coq_forall in @@ -1409,7 +1410,7 @@ module Strategies = let sigma = Sigma.Unsafe.of_evar_map (goalevars evars) in let Sigma (t', sigma, _) = rfn.Reductionops.e_redfun env sigma (EConstr.of_constr t) in let evars' = Sigma.to_evar_map sigma in - if eq_constr t' t then + if Termops.eq_constr evars' (EConstr.of_constr t') (EConstr.of_constr t) then state, Identity else state, Success { rew_car = ty; rew_from = t; rew_to = t'; @@ -1553,14 +1554,15 @@ let assert_replacing id newt tac = in let env' = Environ.reset_with_named_context (val_of_named_context nc) env in Refine.refine ~unsafe:false { run = begin fun sigma -> + let open EConstr in let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma (EConstr.of_constr concl) in let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in let map d = let n = NamedDecl.get_id d in - if Id.equal n id then ev' else mkVar n + if Id.equal n id then ev' else EConstr.mkVar n in - let (e, _) = destEvar ev in - Sigma (EConstr.of_constr (mkEvar (e, Array.map_of_list map nc)), sigma, p +> q) + let (e, _) = EConstr.destEvar (Sigma.to_evar_map sigma) ev in + Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q) end } end } in Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac) @@ -1596,16 +1598,18 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = convert_hyp_no_check (LocalAssum (id, newt)) <*> beta_hyp id | None, Some p -> + let p = EConstr.of_constr p in Proofview.Unsafe.tclEVARS undef <*> Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let make = { run = begin fun sigma -> let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in - Sigma (EConstr.of_constr (mkApp (p, [| ev |])), sigma, q) + Sigma (EConstr.mkApp (p, [| ev |]), sigma, q) end } in Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls end } | None, None -> + let newt = EConstr.of_constr newt in Proofview.Unsafe.tclEVARS undef <*> convert_concl_no_check newt DEFAULTcast in @@ -2168,7 +2172,7 @@ let setoid_reflexivity = tac_open (poly_proof PropGlobal.get_reflexive_proof TypeGlobal.get_reflexive_proof env evm car rel) - (fun c -> tclCOMPLETE (apply c))) + (fun c -> tclCOMPLETE (apply (EConstr.of_constr c)))) (reflexivity_red true) let setoid_symmetry = @@ -2177,7 +2181,7 @@ let setoid_symmetry = tac_open (poly_proof PropGlobal.get_symmetric_proof TypeGlobal.get_symmetric_proof env evm car rel) - (fun c -> apply c)) + (fun c -> apply (EConstr.of_constr c))) (symmetry_red true) let setoid_transitivity c = @@ -2186,8 +2190,8 @@ let setoid_transitivity c = tac_open (poly_proof PropGlobal.get_transitive_proof TypeGlobal.get_transitive_proof env evm car rel) (fun proof -> match c with - | None -> eapply proof - | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ]))) + | None -> eapply (EConstr.of_constr proof) + | Some c -> apply_with_bindings (EConstr.of_constr proof,ImplicitBindings [ c ]))) (transitivity_red true c) let setoid_symmetry_in id = @@ -2204,10 +2208,11 @@ let setoid_symmetry_in id = let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in let new_hyp' = mkApp (he, [| c2 ; c1 |]) in let new_hyp = it_mkProd_or_LetIn new_hyp' binders in + let new_hyp = EConstr.of_constr new_hyp in Proofview.V82.of_tactic (tclTHENLAST (Tactics.assert_after_replacing id new_hyp) - (tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ])) + (tclTHENLIST [ intros; setoid_symmetry; apply (EConstr.mkVar id); Tactics.assumption ])) gl) let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli index 35c4483513..bf56eec10e 100644 --- a/ltac/rewrite.mli +++ b/ltac/rewrite.mli @@ -105,7 +105,7 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic val setoid_reflexivity : unit Proofview.tactic -val setoid_transitivity : constr option -> unit Proofview.tactic +val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic val apply_strategy : diff --git a/ltac/tacexpr.mli b/ltac/tacexpr.mli index 9c25a16457..b8d2d42b7d 100644 --- a/ltac/tacexpr.mli +++ b/ltac/tacexpr.mli @@ -120,9 +120,9 @@ type glob_constr_pattern_and_expr = binding_bound_vars * glob_constr_and_expr * type 'a delayed_open = 'a Tactypes.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } -type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open +type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open -type delayed_open_constr = Term.constr delayed_open +type delayed_open_constr = EConstr.constr delayed_open type intro_pattern = delayed_open_constr intro_pattern_expr located type intro_patterns = delayed_open_constr intro_pattern_expr located list @@ -354,7 +354,7 @@ type raw_tactic_arg = (** Interpreted tactics *) -type t_trm = Term.constr +type t_trm = EConstr.constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 142f061b5a..5535656391 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -746,11 +746,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let interp_constr_with_occurrences_and_name_as_list = interp_constr_in_compound_list - (fun c -> ((AllOccurrences,c),Anonymous)) + (fun c -> ((AllOccurrences,EConstr.of_constr c),Anonymous)) (function ((occs,c),Anonymous) when occs == AllOccurrences -> c | _ -> raise Not_found) (fun ist env sigma (occ_c,na) -> let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in + let c_interp = (fst c_interp, EConstr.of_constr (snd c_interp)) in sigma, (c_interp, interp_name ist env sigma na)) @@ -853,7 +854,7 @@ let rec message_of_value v = Ftactic.return (int (out_gen (topwit wit_int) v)) else if has_type v (topwit wit_intro_pattern) then let p = out_gen (topwit wit_intro_pattern) v in - let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in + let print env sigma c = pr_constr_env env sigma (EConstr.Unsafe.to_constr (fst (Tactics.run_delayed env Evd.empty c))) in Ftactic.nf_enter { enter = begin fun gl -> Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (project gl) c) p) end } @@ -917,6 +918,7 @@ and interp_intro_pattern_action ist env sigma = function let c = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr ist env sigma c in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) } in let sigma,ipat = interp_intro_pattern ist env sigma ipat in @@ -1002,6 +1004,8 @@ let interp_bindings ist env sigma = function let interp_constr_with_bindings ist env sigma (c,bl) = let sigma, bl = interp_bindings ist env sigma bl in let sigma, c = interp_open_constr ist env sigma c in + let c = EConstr.of_constr c in + let bl = Miscops.map_bindings EConstr.of_constr bl in sigma, (c,bl) let interp_open_constr_with_bindings ist env sigma (c,bl) = @@ -1021,6 +1025,7 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr_with_bindings ist env sigma cb in + let c = Miscops.map_with_bindings EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) } in (loc,f) @@ -1044,7 +1049,7 @@ let interp_destruction_arg ist gl arg = then keep,ElimOnIdent (loc,id') else (keep, ElimOnConstr { delayed = begin fun env sigma -> - try Sigma.here (constr_of_id env id', NoBindings) sigma + try Sigma.here (EConstr.of_constr (constr_of_id env id'), NoBindings) sigma with Not_found -> user_err ~loc ~hdr:"interp_destruction_arg" ( pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") @@ -1066,7 +1071,7 @@ let interp_destruction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) } + | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) } with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then @@ -1076,6 +1081,7 @@ let interp_destruction_arg ist gl arg = let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma,c) = interp_open_constr ist env sigma c in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair ((c,NoBindings), sigma) } in keep,ElimOnConstr f @@ -1701,7 +1707,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = pf_env gl in let f sigma (id,n,c) = let (sigma,c_interp) = interp_type ist env sigma c in - sigma , (interp_ident ist env sigma id,n,c_interp) in + sigma , (interp_ident ist env sigma id,n,EConstr.of_constr c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in @@ -1716,7 +1722,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = pf_env gl in let f sigma (id,c) = let (sigma,c_interp) = interp_type ist env sigma c in - sigma , (interp_ident ist env sigma id,c_interp) in + sigma , (interp_ident ist env sigma id,EConstr.of_constr c_interp) in let (sigma,l_interp) = Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl) in @@ -1731,6 +1737,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let (sigma,c) = (if Option.is_empty t then interp_constr else interp_type) ist env sigma c in + let c = EConstr.of_constr c in let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in let tac = Option.map (Option.map (interp_tactic ist)) t in Tacticals.New.tclWITHHOLES false @@ -1758,6 +1765,7 @@ and interp_atomic ist tac : unit Proofview.tactic = if Locusops.is_nowhere clp then (* We try to fully-typecheck the term *) let (sigma,c_interp) = interp_constr ist env sigma c in + let c_interp = EConstr.of_constr c_interp in let let_tac b na c cl eqpat = let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in let with_eq = if b then None else Some (true,id) in @@ -1776,11 +1784,12 @@ and interp_atomic ist tac : unit Proofview.tactic = Tactics.letin_pat_tac with_eq na c cl in let (sigma',c) = interp_pure_open_constr ist env sigma c in + let c = EConstr.of_constr c in name_atomic ~env (TacLetTac(na,c,clp,b,eqpat)) (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_name ist env sigma na) - ((sigma,sigma'),EConstr.of_constr c) clp eqpat) sigma') + ((sigma,sigma'),c) clp eqpat) sigma') end } (* Derived basic tactics *) @@ -1845,6 +1854,7 @@ and interp_atomic ist tac : unit Proofview.tactic = then interp_type ist (pf_env gl) sigma c else interp_constr ist (pf_env gl) sigma c in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) end } in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) @@ -1868,6 +1878,7 @@ and interp_atomic ist tac : unit Proofview.tactic = try let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_constr ist env sigma c in + let c = EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) with e when to_catch e (* Hack *) -> user_err (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") @@ -1884,6 +1895,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let f = { delayed = fun env sigma -> let sigma = Sigma.to_evar_map sigma in let (sigma, c) = interp_open_constr_with_bindings ist env sigma c in + let c = Miscops.map_with_bindings EConstr.of_constr c in Sigma.Unsafe.of_pair (c, sigma) } in (b,m,keep,f)) l in @@ -1906,6 +1918,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | None -> sigma , None | Some c -> let (sigma,c_interp) = interp_constr ist env sigma c in + let c_interp = EConstr.of_constr c_interp in sigma , Some c_interp in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in @@ -1932,6 +1945,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = project gl in let (sigma,c_interp) = interp_constr ist env sigma c in + let c_interp = EConstr.of_constr c_interp in let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in let hyps = interp_hyp_list ist env sigma idl in let tac = name_atomic ~env @@ -2041,6 +2055,7 @@ end } let interp_bindings' ist bl = Ftactic.return { delayed = fun env sigma -> let (sigma, bl) = interp_bindings ist env (Sigma.to_evar_map sigma) bl in + let bl = Miscops.map_bindings EConstr.of_constr bl in Sigma.Unsafe.of_pair (bl, sigma) } diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 11996af731..e3f5342ded 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -161,8 +161,9 @@ let flatten_contravariant_conj _ ist = | Some (_,args) -> let args = List.map EConstr.Unsafe.to_constr args in let newtyp = List.fold_right mkArrow args c in + let newtyp = EConstr.of_constr newtyp in let intros = tclMAP (fun _ -> intro) args in - let by = tclTHENLIST [intros; apply hyp; split; assumption] in + let by = tclTHENLIST [intros; apply (EConstr.of_constr hyp); split; assumption] in tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)] | _ -> fail @@ -186,17 +187,17 @@ let flatten_contravariant_disj _ ist = let typ = assoc_var "X1" ist in let typ = EConstr.of_constr typ in let c = assoc_var "X2" ist in + let c = EConstr.of_constr c in let hyp = assoc_var "id" ist in match match_with_disjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let args = List.map EConstr.Unsafe.to_constr args in let map i arg = - let typ = mkArrow arg c in + let typ = EConstr.mkArrow arg c in let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in - let by = tclTHENLIST [intro; apply hyp; ci; assumption] in + let by = tclTHENLIST [intro; apply (EConstr.of_constr hyp); ci; assumption] in assert_ ~by typ in let tacs = List.mapi map args in @@ -231,6 +232,7 @@ let apply_nnpp _ ist = (Proofview.tclUNIT ()) begin fun () -> try let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in + let nnpp = EConstr.of_constr nnpp in apply nnpp with Not_found -> tclFAIL 0 (Pp.mt ()) end -- cgit v1.2.3