aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'ltac')
-rw-r--r--ltac/coretactics.ml420
-rw-r--r--ltac/evar_tactics.ml5
-rw-r--r--ltac/evar_tactics.mli2
-rw-r--r--ltac/extraargs.mli4
-rw-r--r--ltac/extratactics.ml461
-rw-r--r--ltac/g_auto.ml412
-rw-r--r--ltac/g_class.ml48
-rw-r--r--ltac/g_eqdecide.ml42
-rw-r--r--ltac/g_rewrite.ml42
-rw-r--r--ltac/pptactic.ml32
-rw-r--r--ltac/pptactic.mli4
-rw-r--r--ltac/pptacticsig.mli2
-rw-r--r--ltac/taccoerce.ml57
-rw-r--r--ltac/taccoerce.mli25
-rw-r--r--ltac/tacinterp.ml130
-rw-r--r--ltac/tacinterp.mli1
-rw-r--r--ltac/tactic_debug.ml15
-rw-r--r--ltac/tactic_debug.mli7
-rw-r--r--ltac/tauto.ml2
19 files changed, 189 insertions, 202 deletions
diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index 20d9640fc..28ff6df83 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 (EConstr.of_constr c) ]
+ [ "exact" casted_constr(c) ] -> [ Tactics.exact_no_check c ]
END
TACTIC EXTEND assumption
@@ -39,35 +39,35 @@ TACTIC EXTEND etransitivity
END
TACTIC EXTEND cut
- [ "cut" constr(c) ] -> [ Tactics.cut (EConstr.of_constr c) ]
+ [ "cut" constr(c) ] -> [ Tactics.cut c ]
END
TACTIC EXTEND exact_no_check
- [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check (EConstr.of_constr c) ]
+ [ "exact_no_check" constr(c) ] -> [ Tactics.exact_no_check c ]
END
TACTIC EXTEND vm_cast_no_check
- [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check (EConstr.of_constr c) ]
+ [ "vm_cast_no_check" constr(c) ] -> [ Tactics.vm_cast_no_check c ]
END
TACTIC EXTEND native_cast_no_check
- [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check (EConstr.of_constr c) ]
+ [ "native_cast_no_check" constr(c) ] -> [ Tactics.native_cast_no_check c ]
END
TACTIC EXTEND casetype
- [ "casetype" constr(c) ] -> [ Tactics.case_type (EConstr.of_constr c) ]
+ [ "casetype" constr(c) ] -> [ Tactics.case_type c ]
END
TACTIC EXTEND elimtype
- [ "elimtype" constr(c) ] -> [ Tactics.elim_type (EConstr.of_constr c) ]
+ [ "elimtype" constr(c) ] -> [ Tactics.elim_type c ]
END
TACTIC EXTEND lapply
- [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply (EConstr.of_constr c) ]
+ [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ]
END
TACTIC EXTEND transitivity
- [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some (EConstr.of_constr c)) ]
+ [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ]
END
(** Left *)
@@ -297,7 +297,7 @@ END
(* Generalize dependent *)
TACTIC EXTEND generalize_dependent
- [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep (EConstr.of_constr c) ]
+ [ "generalize" "dependent" constr(c) ] -> [ Tactics.generalize_dep c ]
END
(* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 99023fdbb..6b94da28a 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -77,15 +77,16 @@ let let_evar name typ =
let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let sigma = ref sigma in
- let _ = Typing.e_sort_of env sigma (EConstr.of_constr typ) in
+ let _ = Typing.e_sort_of env sigma typ in
let sigma = Sigma.Unsafe.of_evar_map !sigma in
let id = match name with
| Names.Anonymous ->
+ let typ = EConstr.Unsafe.to_constr typ in
let id = Namegen.id_of_name_using_hdchar env typ name in
Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
| Names.Name id -> id
in
- let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) (EConstr.of_constr typ) in
+ let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
let tac =
(Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
in
diff --git a/ltac/evar_tactics.mli b/ltac/evar_tactics.mli
index e67540c05..41266e61c 100644
--- a/ltac/evar_tactics.mli
+++ b/ltac/evar_tactics.mli
@@ -16,4 +16,4 @@ val instantiate_tac : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
val instantiate_tac_by_name : Id.t ->
Tacinterp.interp_sign * Glob_term.glob_constr -> unit Proofview.tactic
-val let_evar : Name.t -> Term.types -> unit Proofview.tactic
+val let_evar : Name.t -> EConstr.types -> unit Proofview.tactic
diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli
index b12187e18..7d4bccfad 100644
--- a/ltac/extraargs.mli
+++ b/ltac/extraargs.mli
@@ -38,12 +38,12 @@ val wit_lglob :
val wit_lconstr :
(constr_expr,
Tacexpr.glob_constr_and_expr,
- Constr.t) Genarg.genarg_type
+ EConstr.t) Genarg.genarg_type
val wit_casted_constr :
(constr_expr,
Tacexpr.glob_constr_and_expr,
- Constr.t) Genarg.genarg_type
+ EConstr.t) Genarg.genarg_type
val glob : constr_expr Pcoq.Gram.entry
val lglob : constr_expr Pcoq.Gram.entry
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index bf8481b52..65c75703b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -47,16 +47,16 @@ let with_delayed_uconstr ist c tac =
let replace_in_clause_maybe_by ist c1 c2 cl tac =
with_delayed_uconstr ist c1
- (fun c1 -> replace_in_clause_maybe_by (EConstr.of_constr c1) c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
+ (fun c1 -> replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac))
let replace_term ist dir_opt c cl =
- with_delayed_uconstr ist c (fun c -> replace_term dir_opt (EConstr.of_constr c) cl)
+ with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl)
let clause = Pltac.clause_dft_concl
TACTIC EXTEND replace
["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ]
--> [ replace_in_clause_maybe_by ist c1 (EConstr.of_constr c2) cl tac ]
+-> [ replace_in_clause_maybe_by ist c1 c2 cl tac ]
END
TACTIC EXTEND replace_term_left
@@ -153,9 +153,9 @@ let injHyp id =
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 (EConstr.of_constr c) ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
- -> [ rewriteInHyp b (EConstr.of_constr c) id ]
+ -> [ rewriteInHyp b c id ]
END
(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to
@@ -163,20 +163,20 @@ END
"cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *)
TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b (EConstr.of_constr eqn) ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
- -> [ cutRewriteInHyp b (EConstr.of_constr eqn) id ]
+ -> [ cutRewriteInHyp b eqn id ]
END
(**********************************************************************)
(* Decompose *)
TACTIC EXTEND decompose_sum
-| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or (EConstr.of_constr c) ]
+| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ]
END
TACTIC EXTEND decompose_record
-| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and (EConstr.of_constr c) ]
+| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ]
END
(**********************************************************************)
@@ -185,7 +185,7 @@ END
open Contradiction
TACTIC EXTEND absurd
- [ "absurd" constr(c) ] -> [ absurd (EConstr.of_constr c) ]
+ [ "absurd" constr(c) ] -> [ absurd c ]
END
let onSomeWithHoles tac = function
@@ -235,7 +235,7 @@ END
let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) =
let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in
with_delayed_uconstr ist c
- (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (EConstr.of_constr c,NoBindings) true)
+ (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true)
TACTIC EXTEND rewrite_star
| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
@@ -362,7 +362,7 @@ let refine_tac ist simple c =
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma ->
let Sigma (c, sigma, p) = c.delayed env sigma in
- Sigma (EConstr.of_constr c, sigma, p)
+ Sigma (c, sigma, p)
} in
let refine = Refine.refine ~unsafe:true update in
if simple then refine
@@ -516,13 +516,13 @@ let add_transitivity_lemma left lem =
(* Vernacular syntax *)
TACTIC EXTEND stepl
-| ["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 ()) ]
+| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ]
+| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ]
END
TACTIC EXTEND stepr
-| ["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 ()) ]
+| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ]
+| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ]
END
VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF
@@ -645,6 +645,8 @@ let subst_hole_with_term occ tc t =
open Tacmach
let hResolve id c occ t =
+ let c = EConstr.Unsafe.to_constr c in
+ let t = EConstr.Unsafe.to_constr t in
Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let sigma = Sigma.to_evar_map sigma in
@@ -819,8 +821,9 @@ END
let eq_constr x y =
Proofview.Goal.enter { enter = begin fun gl ->
let evd = Tacmach.New.project gl in
- if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT ()
- else Tacticals.New.tclFAIL 0 (str "Not equal")
+ match EConstr.eq_constr_universes evd x y with
+ | Some _ -> Proofview.tclUNIT ()
+ | None -> Tacticals.New.tclFAIL 0 (str "Not equal")
end }
TACTIC EXTEND constr_eq
@@ -830,15 +833,13 @@ END
TACTIC EXTEND constr_eq_nounivs
| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- let x = EConstr.of_constr x in
- let y = EConstr.of_constr y in
if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ]
END
TACTIC EXTEND is_evar
| [ "is_evar" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Evar _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (str "Not an evar")
]
@@ -871,14 +872,14 @@ has_evar c
TACTIC EXTEND has_evar
| [ "has_evar" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- if has_evar sigma (EConstr.of_constr x) then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars")
+ if has_evar sigma x then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "No evars")
]
END
TACTIC EXTEND is_hyp
| [ "is_var" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Var _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ]
END
@@ -886,7 +887,7 @@ END
TACTIC EXTEND is_fix
| [ "is_fix" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Fix _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ]
END;;
@@ -894,7 +895,7 @@ END;;
TACTIC EXTEND is_cofix
| [ "is_cofix" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| CoFix _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ]
END;;
@@ -902,7 +903,7 @@ END;;
TACTIC EXTEND is_ind
| [ "is_ind" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Ind _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ]
END;;
@@ -910,7 +911,7 @@ END;;
TACTIC EXTEND is_constructor
| [ "is_constructor" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Construct _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ]
END;;
@@ -918,7 +919,7 @@ END;;
TACTIC EXTEND is_proj
| [ "is_proj" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Proj _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ]
END;;
@@ -926,7 +927,7 @@ END;;
TACTIC EXTEND is_const
| [ "is_const" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- match EConstr.kind sigma (EConstr.of_constr x) with
+ match EConstr.kind sigma x with
| Const _ -> Proofview.tclUNIT ()
| _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ]
END;;
@@ -1080,7 +1081,7 @@ let decompose l c =
end }
TACTIC EXTEND decompose
-| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose (List.map EConstr.of_constr l) (EConstr.of_constr c) ]
+| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
END
(** library/keys *)
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index b5e56d93b..d4d3b9d66 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -28,7 +28,7 @@ TACTIC EXTEND eassumption
END
TACTIC EXTEND eexact
-| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact (EConstr.of_constr c) ]
+| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ]
END
let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases
@@ -51,7 +51,7 @@ let eval_uconstrs ist cs =
} in
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)
+ Sigma.Sigma (c, sigma, p)
} in
List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs
@@ -151,7 +151,7 @@ TACTIC EXTEND autounfold_one
TACTIC EXTEND autounfoldify
| [ "autounfoldify" constr(x) ] -> [
Proofview.tclEVARMAP >>= fun sigma ->
- let db = match EConstr.kind sigma (EConstr.of_constr x) with
+ let db = match EConstr.kind sigma x with
| Term.Const (c,_) -> Names.Label.to_string (Names.con_label c)
| _ -> assert false
in Eauto.autounfold ["core";db] Locusops.onConcl
@@ -159,7 +159,7 @@ TACTIC EXTEND autounfoldify
END
TACTIC EXTEND unify
-| ["unify" constr(x) constr(y) ] -> [ Tactics.unify (EConstr.of_constr x) (EConstr.of_constr y) ]
+| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x 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
@@ -168,13 +168,13 @@ TACTIC EXTEND unify
Tacticals.New.tclZEROMSG msg
| Some t ->
let state = Hints.Hint_db.transparent_state t in
- Tactics.unify ~state (EConstr.of_constr x) (EConstr.of_constr y)
+ Tactics.unify ~state x y
]
END
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check (EConstr.of_constr x) Term.DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
END
let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4
index a983a4fea..b7f0881f1 100644
--- a/ltac/g_class.ml4
+++ b/ltac/g_class.ml4
@@ -62,19 +62,19 @@ TACTIC EXTEND typeclasses_eauto
END
TACTIC EXTEND head_of_constr
- [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h (EConstr.of_constr c) ]
+ [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ]
END
TACTIC EXTEND not_evar
- [ "not_evar" constr(ty) ] -> [ not_evar (EConstr.of_constr ty) ]
+ [ "not_evar" constr(ty) ] -> [ not_evar ty ]
END
TACTIC EXTEND is_ground
- [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground (EConstr.of_constr ty)) ]
+ [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
END
TACTIC EXTEND autoapply
- [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply (EConstr.of_constr c) i) ]
+ [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ]
END
(** TODO: DEPRECATE *)
diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 6a49ea830..905653281 100644
--- a/ltac/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
@@ -23,5 +23,5 @@ TACTIC EXTEND decide_equality
END
TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare (EConstr.of_constr c1) (EConstr.of_constr c2) ]
+| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
END
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index bae5a516c..b1c4f58eb 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 (EConstr.of_constr t)) ]
+ [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ]
| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ]
END
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index 934830f4d..b7dd37cdd 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -59,8 +59,8 @@ type 'a glob_extra_genarg_printer =
'a -> std_ppcmds
type 'a extra_genarg_printer =
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
+ (EConstr.constr -> std_ppcmds) ->
+ (EConstr.constr -> std_ppcmds) ->
(tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
@@ -1167,15 +1167,15 @@ module Make
| _ -> error "Cannot translate fix tactic: not enough products" in
strip_ty [] n ty
- let pr_atomic_tactic_level env n t =
+ let pr_atomic_tactic_level env sigma n t =
let prtac n (t:atomic_tactic_expr) =
let pr = {
pr_tactic = (fun _ _ -> str "<tactic>");
- pr_constr = (fun c -> pr_constr_env env Evd.empty (EConstr.Unsafe.to_constr c));
+ pr_constr = (fun c -> pr_econstr_env env sigma c);
pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
- 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_lconstr = (fun c -> pr_leconstr_env env sigma c);
+ pr_pattern = pr_constr_pattern_env env sigma;
+ pr_lpattern = pr_lconstr_pattern_env env sigma;
pr_constant = pr_evaluable_reference_env env;
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
@@ -1206,7 +1206,7 @@ module Make
let pr_extend pr lev ml args =
pr_extend_gen pr lev ml args
- let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
+ let pr_atomic_tactic env sigma c = pr_atomic_tactic_level env sigma ltop c
end
@@ -1255,7 +1255,7 @@ let declare_extra_genarg_pprule wit
in
let h x =
let env = Global.env () in
- h (pr_constr_env env Evd.empty) (pr_lconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
+ h (pr_econstr_env env Evd.empty) (pr_leconstr_env env Evd.empty) (fun _ _ -> str "<tactic>") x
in
Genprint.register_print0 wit f g h
@@ -1285,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 (EConstr.Unsafe.to_constr (fst (run_delayed c)))));
+ (Miscprint.pr_intro_pattern (fun c -> pr_econstr (fst (run_delayed c))));
Genprint.register_print0
wit_clause_dft_concl
(pr_clauses (Some true) pr_lident)
@@ -1296,7 +1296,7 @@ let () =
wit_constr
Ppconstr.pr_constr_expr
(fun (c, _) -> Printer.pr_glob_constr c)
- Printer.pr_constr
+ Printer.pr_econstr
;
Genprint.register_print0
wit_uconstr
@@ -1308,25 +1308,25 @@ let () =
wit_open_constr
Ppconstr.pr_constr_expr
(fun (c, _) -> Printer.pr_glob_constr c)
- Printer.pr_constr
+ Printer.pr_econstr
;
Genprint.register_print0 wit_red_expr
(pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))
(pr_red_expr (pr_and_constr_expr pr_glob_constr, pr_and_constr_expr pr_lglob_constr, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr))
- (pr_red_expr (pr_constr, pr_lconstr, pr_evaluable_reference, pr_constr_pattern));
+ (pr_red_expr (pr_econstr, pr_leconstr, pr_evaluable_reference, pr_constr_pattern));
Genprint.register_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
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 (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it)));
+ (fun it -> pr_bindings_no_with pr_econstr pr_leconstr (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 (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (fst (run_delayed it)));
+ (fun it -> pr_with_bindings pr_econstr pr_leconstr (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 (EConstr.Unsafe.to_constr %> pr_constr) (EConstr.Unsafe.to_constr %> pr_lconstr) (run_delayed_destruction_arg it));
+ (fun it -> pr_destruction_arg pr_econstr pr_leconstr (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/pptactic.mli b/ltac/pptactic.mli
index 86e3ea548..5fff3062d 100644
--- a/ltac/pptactic.mli
+++ b/ltac/pptactic.mli
@@ -34,8 +34,8 @@ type 'a glob_extra_genarg_printer =
'a -> std_ppcmds
type 'a extra_genarg_printer =
- (Term.constr -> std_ppcmds) ->
- (Term.constr -> std_ppcmds) ->
+ (EConstr.constr -> std_ppcmds) ->
+ (EConstr.constr -> std_ppcmds) ->
(tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
diff --git a/ltac/pptacticsig.mli b/ltac/pptacticsig.mli
index 74ddd377a..dfbc3b3ed 100644
--- a/ltac/pptacticsig.mli
+++ b/ltac/pptacticsig.mli
@@ -61,7 +61,7 @@ module type Pp = sig
val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
- val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+ val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds
val pr_hintbases : string list option -> std_ppcmds
diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml
index 288e12d0b..114b8dda0 100644
--- a/ltac/taccoerce.ml
+++ b/ltac/taccoerce.ml
@@ -9,6 +9,7 @@
open Util
open Names
open Term
+open EConstr
open Pattern
open Misctypes
open Genarg
@@ -64,7 +65,7 @@ let to_constr v =
Some c
else if has_type v (topwit wit_constr_under_binders) then
let vars, c = out_gen (topwit wit_constr_under_binders) v in
- match vars with [] -> Some (EConstr.Unsafe.to_constr c) | _ -> None
+ match vars with [] -> Some c | _ -> None
else None
let of_uconstr c = in_gen (topwit wit_uconstr) c
@@ -106,7 +107,7 @@ let coerce_to_constr_context v =
else raise (CannotCoerceTo "a term context")
(* Interprets an identifier which must be fresh *)
-let coerce_var_to_ident fresh env v =
+let coerce_var_to_ident fresh env sigma v =
let v = Value.normalize v in
let fail () = raise (CannotCoerceTo "a fresh identifier") in
if has_type v (topwit wit_intro_pattern) then
@@ -119,15 +120,16 @@ let coerce_var_to_ident fresh env v =
| None -> fail ()
| Some c ->
(* We need it fresh for intro e.g. in "Tac H = clear H; intro H" *)
- if isVar c && not (fresh && is_variable env (destVar c)) then
- destVar c
+ if isVar sigma c && not (fresh && is_variable env (destVar sigma c)) then
+ destVar sigma c
else fail ()
(* Interprets, if possible, a constr to an identifier which may not
be fresh but suitable to be given to the fresh tactic. Works for
vars, constants, inductive, constructors and sorts. *)
-let coerce_to_ident_not_fresh g env v =
+let coerce_to_ident_not_fresh env sigma v =
+let g = sigma in
let id_of_name = function
| Names.Anonymous -> Id.of_string "x"
| Names.Name x -> x in
@@ -143,7 +145,7 @@ let id_of_name = function
match Value.to_constr v with
| None -> fail ()
| Some c ->
- match Constr.kind c with
+ match EConstr.kind sigma c with
| Var id -> id
| Meta m -> id_of_name (Evd.meta_name g m)
| Evar (kn,_) ->
@@ -169,7 +171,7 @@ let id_of_name = function
| _ -> fail()
-let coerce_to_intro_pattern env v =
+let coerce_to_intro_pattern env sigma v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
snd (out_gen (topwit wit_intro_pattern) v)
@@ -177,14 +179,14 @@ let coerce_to_intro_pattern env v =
let id = out_gen (topwit wit_var) v in
IntroNaming (IntroIdentifier id)
else match Value.to_constr v with
- | Some c when isVar c ->
+ | Some c when isVar sigma c ->
(* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
(* but also in "destruct H as (H,H')" *)
- IntroNaming (IntroIdentifier (destVar c))
+ IntroNaming (IntroIdentifier (destVar sigma c))
| _ -> raise (CannotCoerceTo "an introduction pattern")
-let coerce_to_intro_pattern_naming env v =
- match coerce_to_intro_pattern env v with
+let coerce_to_intro_pattern_naming env sigma v =
+ match coerce_to_intro_pattern env sigma v with
| IntroNaming pat -> pat
| _ -> raise (CannotCoerceTo "a naming introduction pattern")
@@ -212,7 +214,7 @@ let coerce_to_constr env v =
| _ -> fail ()
else if has_type v (topwit wit_constr) then
let c = out_gen (topwit wit_constr) v in
- ([], EConstr.of_constr c)
+ ([], c)
else if has_type v (topwit wit_constr_under_binders) then
out_gen (topwit wit_constr_under_binders) v
else if has_type v (topwit wit_var) then
@@ -229,11 +231,10 @@ let coerce_to_uconstr env v =
let coerce_to_closed_constr env v =
let ids,c = coerce_to_constr env v in
- let c = EConstr.Unsafe.to_constr c in
let () = if not (List.is_empty ids) then raise (CannotCoerceTo "a term") in
c
-let coerce_to_evaluable_ref env v =
+let coerce_to_evaluable_ref env sigma v =
let fail () = raise (CannotCoerceTo "an evaluable reference") in
let v = Value.normalize v in
let ev =
@@ -254,8 +255,8 @@ let coerce_to_evaluable_ref env v =
| IndRef _ | ConstructRef _ -> fail ()
else
match Value.to_constr v with
- | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c))
- | Some c when isVar c -> EvalVarRef (destVar c)
+ | Some c when isConst sigma c -> EvalConstRef (Univ.out_punivs (destConst sigma c))
+ | Some c when isVar sigma c -> EvalVarRef (destVar sigma c)
| _ -> fail ()
in if Tacred.is_evaluable env ev then ev else fail ()
@@ -267,14 +268,14 @@ let coerce_to_constr_list env v =
List.map map l
| None -> raise (CannotCoerceTo "a term list")
-let coerce_to_intro_pattern_list loc env v =
+let coerce_to_intro_pattern_list loc env sigma v =
match Value.to_list v with
| None -> raise (CannotCoerceTo "an intro pattern list")
| Some l ->
- let map v = (loc, coerce_to_intro_pattern env v) in
+ let map v = (loc, coerce_to_intro_pattern env sigma v) in
List.map map l
-let coerce_to_hyp env v =
+let coerce_to_hyp env sigma v =
let fail () = raise (CannotCoerceTo "a variable") in
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
@@ -285,31 +286,31 @@ let coerce_to_hyp env v =
let id = out_gen (topwit wit_var) v in
if is_variable env id then id else fail ()
else match Value.to_constr v with
- | Some c when isVar c -> destVar c
+ | Some c when isVar sigma c -> destVar sigma c
| _ -> fail ()
-let coerce_to_hyp_list env v =
+let coerce_to_hyp_list env sigma v =
let v = Value.to_list v in
match v with
| Some l ->
- let map n = coerce_to_hyp env n in
+ let map n = coerce_to_hyp env sigma n in
List.map map l
| None -> raise (CannotCoerceTo "a variable list")
(* Interprets a qualified name *)
-let coerce_to_reference env v =
+let coerce_to_reference env sigma v =
let v = Value.normalize v in
match Value.to_constr v with
| Some c ->
begin
- try Globnames.global_of_constr c
+ try fst (Termops.global_of_constr sigma c)
with Not_found -> raise (CannotCoerceTo "a reference")
end
| None -> raise (CannotCoerceTo "a reference")
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
-let coerce_to_quantified_hypothesis v =
+let coerce_to_quantified_hypothesis sigma v =
let v = Value.normalize v in
if has_type v (topwit wit_intro_pattern) then
let v = out_gen (topwit wit_intro_pattern) v in
@@ -322,17 +323,17 @@ let coerce_to_quantified_hypothesis v =
else if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
else match Value.to_constr v with
- | Some c when isVar c -> NamedHyp (destVar c)
+ | Some c when isVar sigma c -> NamedHyp (destVar sigma c)
| _ -> raise (CannotCoerceTo "a quantified hypothesis")
(* Quantified named or numbered hypothesis or hypothesis in context *)
(* (as in Inversion) *)
-let coerce_to_decl_or_quant_hyp env v =
+let coerce_to_decl_or_quant_hyp env sigma v =
let v = Value.normalize v in
if has_type v (topwit wit_int) then
AnonHyp (out_gen (topwit wit_int) v)
else
- try coerce_to_quantified_hypothesis v
+ try coerce_to_quantified_hypothesis sigma v
with CannotCoerceTo _ ->
raise (CannotCoerceTo "a declared or quantified hypothesis")
diff --git a/ltac/taccoerce.mli b/ltac/taccoerce.mli
index 3049aff7e..9c4ac5265 100644
--- a/ltac/taccoerce.mli
+++ b/ltac/taccoerce.mli
@@ -9,6 +9,7 @@
open Util
open Names
open Term
+open EConstr
open Misctypes
open Pattern
open Genarg
@@ -48,16 +49,16 @@ end
(** {5 Coercion functions} *)
-val coerce_to_constr_context : Value.t -> EConstr.constr
+val coerce_to_constr_context : Value.t -> constr
-val coerce_var_to_ident : bool -> Environ.env -> Value.t -> Id.t
+val coerce_var_to_ident : bool -> Environ.env -> Evd.evar_map -> Value.t -> Id.t
-val coerce_to_ident_not_fresh : Evd.evar_map -> Environ.env -> Value.t -> Id.t
+val coerce_to_ident_not_fresh : Environ.env -> Evd.evar_map -> Value.t -> Id.t
-val coerce_to_intro_pattern : Environ.env -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
+val coerce_to_intro_pattern : Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.delayed_open_constr intro_pattern_expr
val coerce_to_intro_pattern_naming :
- Environ.env -> Value.t -> intro_pattern_naming_expr
+ Environ.env -> Evd.evar_map -> Value.t -> intro_pattern_naming_expr
val coerce_to_hint_base : Value.t -> string
@@ -70,22 +71,22 @@ val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr
val coerce_to_closed_constr : Environ.env -> Value.t -> constr
val coerce_to_evaluable_ref :
- Environ.env -> Value.t -> evaluable_global_reference
+ Environ.env -> Evd.evar_map -> Value.t -> evaluable_global_reference
val coerce_to_constr_list : Environ.env -> Value.t -> constr list
val coerce_to_intro_pattern_list :
- Loc.t -> Environ.env -> Value.t -> Tacexpr.intro_patterns
+ Loc.t -> Environ.env -> Evd.evar_map -> Value.t -> Tacexpr.intro_patterns
-val coerce_to_hyp : Environ.env -> Value.t -> Id.t
+val coerce_to_hyp : Environ.env -> Evd.evar_map -> Value.t -> Id.t
-val coerce_to_hyp_list : Environ.env -> Value.t -> Id.t list
+val coerce_to_hyp_list : Environ.env -> Evd.evar_map -> Value.t -> Id.t list
-val coerce_to_reference : Environ.env -> Value.t -> Globnames.global_reference
+val coerce_to_reference : Environ.env -> Evd.evar_map -> Value.t -> Globnames.global_reference
-val coerce_to_quantified_hypothesis : Value.t -> quantified_hypothesis
+val coerce_to_quantified_hypothesis : Evd.evar_map -> Value.t -> quantified_hypothesis
-val coerce_to_decl_or_quant_hyp : Environ.env -> Value.t -> quantified_hypothesis
+val coerce_to_decl_or_quant_hyp : Environ.env -> Evd.evar_map -> Value.t -> quantified_hypothesis
val coerce_to_int_or_var_list : Value.t -> int or_var list
diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index b4d2b1e50..1fe6dbdd0 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -239,12 +239,12 @@ let pr_value env v =
else if has_type v (topwit wit_constr_context) then
let c = out_gen (topwit wit_constr_context) v in
match env with
- | Some (env,sigma) -> pr_lconstr_env env sigma (EConstr.Unsafe.to_constr c)
+ | Some (env,sigma) -> pr_leconstr_env env sigma c
| _ -> str "a term"
else if has_type v (topwit wit_constr) then
let c = out_gen (topwit wit_constr) v in
match env with
- | Some (env,sigma) -> pr_lconstr_env env sigma c
+ | Some (env,sigma) -> pr_leconstr_env env sigma c
| _ -> str "a term"
else if has_type v (topwit wit_constr_under_binders) then
let c = out_gen (topwit wit_constr_under_binders) v in
@@ -282,7 +282,7 @@ let pr_inspect env expr result =
(* Transforms an id into a constr if possible, or fails with Not_found *)
let constr_of_id env id =
- Term.mkVar (let _ = Environ.lookup_named id env in id)
+ EConstr.mkVar (let _ = Environ.lookup_named id env in id)
(** Generic arguments : table of interpretation functions *)
@@ -334,7 +334,7 @@ let (+++) lfun1 lfun2 = Id.Map.fold Id.Map.add lfun1 lfun2
let extend_values_with_bindings (ln,lm) lfun =
let of_cub c = match c with
- | [], c -> Value.of_constr (EConstr.Unsafe.to_constr c)
+ | [], c -> Value.of_constr c
| _ -> in_gen (topwit wit_constr_under_binders) c
in
(* For compatibility, bound variables are visible only if no other
@@ -385,7 +385,7 @@ let interp_ltac_var coerce ist env locid =
with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time")
let interp_ident ist env sigma id =
- try try_interp_ltac_var (coerce_var_to_ident false env) ist (Some (env,sigma)) (dloc,id)
+ try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (dloc,id)
with Not_found -> id
(* Interprets an optional identifier, bound or fresh *)
@@ -394,11 +394,11 @@ let interp_name ist env sigma = function
| Name id -> Name (interp_ident ist env sigma id)
let interp_intro_pattern_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern env) ist (Some (env,sigma)) (loc,id)
+ try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id)
with Not_found -> IntroNaming (IntroIdentifier id)
let interp_intro_pattern_naming_var loc ist env sigma id =
- try try_interp_ltac_var (coerce_to_intro_pattern_naming env) ist (Some (env,sigma)) (loc,id)
+ try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id)
with Not_found -> IntroIdentifier id
let interp_int ist locid =
@@ -423,14 +423,14 @@ let interp_int_or_var_list ist l =
(* Interprets a bound variable (especially an existing hypothesis) *)
let interp_hyp ist env sigma (loc,id as locid) =
(* Look first in lfun for a value coercible to a variable *)
- try try_interp_ltac_var (coerce_to_hyp env) ist (Some (env,sigma)) locid
+ try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid
with Not_found ->
(* Then look if bound in the proof context at calling time *)
if is_variable env id then id
else Loc.raise ~loc (Logic.RefinerError (Logic.NoSuchHyp id))
let interp_hyp_list_as_list ist env sigma (loc,id as x) =
- try coerce_to_hyp_list env (Id.Map.find id ist.lfun)
+ try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x]
let interp_hyp_list ist env sigma l =
@@ -445,7 +445,7 @@ let interp_move_location ist env sigma = function
let interp_reference ist env sigma = function
| ArgArg (_,r) -> r
| ArgVar (loc, id) ->
- try try_interp_ltac_var (coerce_to_reference env) ist (Some (env,sigma)) (loc, id)
+ try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id)
with Not_found ->
try
VarRef (get_id (Environ.lookup_named id env))
@@ -469,7 +469,7 @@ let interp_evaluable ist env sigma = function
end
| ArgArg (r,None) -> r
| ArgVar (loc, id) ->
- try try_interp_ltac_var (coerce_to_evaluable_ref env) ist (Some (env,sigma)) (loc, id)
+ try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id)
with Not_found ->
try try_interp_evaluable env (loc, id)
with Not_found -> error_global_not_found ~loc (qualid_of_ident id)
@@ -540,7 +540,7 @@ let default_fresh_id = Id.of_string "H"
let interp_fresh_id ist env sigma l =
let extract_ident ist env sigma id =
- try try_interp_ltac_var (coerce_to_ident_not_fresh sigma env)
+ try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma)
ist (Some (env,sigma)) (dloc,id)
with Not_found -> id in
let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in
@@ -561,24 +561,24 @@ let interp_fresh_id ist env sigma l =
Tactics.fresh_id_in_env avoid id env
(* Extract the uconstr list from lfun *)
-let extract_ltac_constr_context ist env =
+let extract_ltac_constr_context ist env sigma =
let open Glob_term in
- let add_uconstr id env v map =
+ let add_uconstr id v map =
try Id.Map.add id (coerce_to_uconstr env v) map
with CannotCoerceTo _ -> map
in
- let add_constr id env v map =
+ let add_constr id v map =
try Id.Map.add id (coerce_to_constr env v) map
with CannotCoerceTo _ -> map
in
- let add_ident id env v map =
- try Id.Map.add id (coerce_var_to_ident false env v) map
+ let add_ident id v map =
+ try Id.Map.add id (coerce_var_to_ident false env sigma v) map
with CannotCoerceTo _ -> map
in
let fold id v {idents;typed;untyped} =
- let idents = add_ident id env v idents in
- let typed = add_constr id env v typed in
- let untyped = add_uconstr id env v untyped in
+ let idents = add_ident id v idents in
+ let typed = add_constr id v typed in
+ let untyped = add_uconstr id v untyped in
{ idents ; typed ; untyped }
in
let empty = { idents = Id.Map.empty ;typed = Id.Map.empty ; untyped = Id.Map.empty } in
@@ -586,11 +586,11 @@ let extract_ltac_constr_context ist env =
(** Significantly simpler than [interp_constr], to interpret an
untyped constr, it suffices to adjoin a closure environment. *)
-let interp_uconstr ist env = function
+let interp_uconstr ist env sigma = function
| (term,None) ->
- { closure = extract_ltac_constr_context ist env ; term }
+ { closure = extract_ltac_constr_context ist env sigma; term }
| (_,Some ce) ->
- let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env in
+ let ( {typed ; untyped } as closure) = extract_ltac_constr_context ist env sigma in
let ltacvars = {
Constrintern.ltac_vars = Id.(Set.union (Map.domain typed) (Map.domain untyped));
ltac_bound = Id.Map.domain ist.lfun;
@@ -598,7 +598,7 @@ let interp_uconstr ist env = function
{ closure ; term = intern_gen WithoutTypeConstraint ~ltacvars env ce }
let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
- let constrvars = extract_ltac_constr_context ist env in
+ let constrvars = extract_ltac_constr_context ist env sigma in
let vars = {
Pretyping.ltac_constrs = constrvars.typed;
Pretyping.ltac_uconstrs = constrvars.untyped;
@@ -636,10 +636,11 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) c
in
+ let c = EConstr.of_constr c in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
- Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
+ Proofview.NonLogical.run (db_constr (curr_debug ist) env evd c);
(evd,c)
let constr_flags = {
@@ -691,7 +692,7 @@ let interp_pure_open_constr ist =
let interp_typed_pattern ist env sigma (_,c,_) =
let sigma, c =
interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
- pattern_of_constr env sigma (EConstr.of_constr c)
+ pattern_of_constr env sigma c
(* Interprets a constr expression *)
let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
@@ -733,10 +734,10 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) =
prioritary to an evaluable reference and otherwise to a constr
(it is an encoding to satisfy the "union" type given to Simpl) *)
let coerce_eval_ref_or_constr x =
- try Inl (coerce_to_evaluable_ref env x)
+ try Inl (coerce_to_evaluable_ref env sigma x)
with CannotCoerceTo _ ->
let c = coerce_to_closed_constr env x in
- Inr (pattern_of_constr env sigma (EConstr.of_constr c)) in
+ Inr (pattern_of_constr env sigma c) in
(try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id)
with Not_found ->
error_global_not_found ~loc (qualid_of_ident id))
@@ -746,12 +747,11 @@ 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,EConstr.of_constr c),Anonymous))
+ (fun c -> ((AllOccurrences,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))
@@ -784,8 +784,7 @@ let interp_may_eval f ist env sigma = function
let (sigma,c_interp) = f ist env sigma c in
let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in
let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma (EConstr.of_constr c_interp) in
- let c = EConstr.Unsafe.to_constr c in
+ let Sigma (c, sigma, _) = redfun.Reductionops.e_redfun env sigma c_interp in
(Sigma.to_evar_map sigma, c)
| ConstrContext ((loc,s),c) ->
(try
@@ -793,8 +792,10 @@ let interp_may_eval f ist env sigma = function
let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
let ctxt = EConstr.Unsafe.to_constr ctxt in
let evdref = ref sigma in
+ let ic = EConstr.Unsafe.to_constr ic in
let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
+ let c = EConstr.of_constr c in
!evdref , c
with
| Not_found ->
@@ -802,8 +803,8 @@ let interp_may_eval f ist env sigma = function
(str "Unbound context identifier" ++ pr_id s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
- let (sigma, t) = Typing.type_of ~refresh:true env sigma (EConstr.of_constr c_interp) in
- (sigma, EConstr.Unsafe.to_constr t)
+ let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in
+ (sigma, t)
| ConstrTerm c ->
try
f ist env sigma c
@@ -833,7 +834,7 @@ let interp_constr_may_eval ist env sigma c =
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
up with any assumption. *)
- Proofview.NonLogical.run (db_constr (curr_debug ist) env csr);
+ Proofview.NonLogical.run (db_constr (curr_debug ist) env sigma csr);
sigma , csr
end
@@ -845,7 +846,7 @@ let rec message_of_value v =
Ftactic.return (str "<tactic>")
else if has_type v (topwit wit_constr) then
let v = out_gen (topwit wit_constr) v in
- Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (project gl) v) end }
+ Ftactic.nf_enter {enter = begin fun gl -> Ftactic.return (pr_econstr_env (pf_env gl) (project gl) v) end }
else if has_type v (topwit wit_constr_under_binders) then
let c = out_gen (topwit wit_constr_under_binders) v in
Ftactic.nf_enter { enter = begin fun gl ->
@@ -922,7 +923,6 @@ 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
@@ -939,7 +939,7 @@ and interp_or_and_intro_pattern ist env sigma = function
and interp_intro_pattern_list_as_list ist env sigma = function
| [loc,IntroNaming (IntroIdentifier id)] as l ->
- (try sigma, coerce_to_intro_pattern_list loc env (Id.Map.find id ist.lfun)
+ (try sigma, coerce_to_intro_pattern_list loc env sigma (Id.Map.find id ist.lfun)
with Not_found | CannotCoerceTo _ ->
List.fold_map (interp_intro_pattern ist env) sigma l)
| l -> List.fold_map (interp_intro_pattern ist env) sigma l
@@ -951,7 +951,7 @@ let interp_intro_pattern_naming_option ist env sigma = function
let interp_or_and_intro_pattern_option ist env sigma = function
| None -> sigma, None
| Some (ArgVar (loc,id)) ->
- (match coerce_to_intro_pattern env (Id.Map.find id ist.lfun) with
+ (match coerce_to_intro_pattern env sigma (Id.Map.find id ist.lfun) with
| IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l)
| _ ->
raise (CannotCoerceTo "a disjunctive/conjunctive introduction pattern"))
@@ -969,31 +969,25 @@ let interp_in_hyp_as ist env sigma (id,ipat) =
let sigma, ipat = interp_intro_pattern_option ist env sigma ipat in
sigma,(interp_hyp ist env sigma id,ipat)
-let interp_quantified_hypothesis ist = function
- | AnonHyp n -> AnonHyp n
- | NamedHyp id ->
- try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
- with Not_found -> NamedHyp id
-
-let interp_binding_name ist = function
+let interp_binding_name ist sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
(* If a name is bound, it has to be a quantified hypothesis *)
(* user has to use other names for variables if these ones clash with *)
(* a name intented to be used as a (non-variable) identifier *)
- try try_interp_ltac_var coerce_to_quantified_hypothesis ist None(dloc,id)
+ try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist None(dloc,id)
with Not_found -> NamedHyp id
let interp_declared_or_quantified_hypothesis ist env sigma = function
| AnonHyp n -> AnonHyp n
| NamedHyp id ->
try try_interp_ltac_var
- (coerce_to_decl_or_quant_hyp env) ist (Some (env,sigma)) (dloc,id)
+ (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (dloc,id)
with Not_found -> NamedHyp id
let interp_binding ist env sigma (loc,b,c) =
let sigma, c = interp_open_constr ist env sigma c in
- sigma, (loc,interp_binding_name ist b,c)
+ sigma, (loc,interp_binding_name ist sigma b,c)
let interp_bindings ist env sigma = function
| NoBindings ->
@@ -1008,14 +1002,11 @@ 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) =
let sigma, bl = interp_bindings ist env sigma bl in
let sigma, c = interp_open_constr ist env sigma c in
- let (c, bl) = Miscops.map_with_bindings EConstr.of_constr (c, bl) in
sigma, (c, bl)
let loc_of_bindings = function
@@ -1053,7 +1044,7 @@ let interp_destruction_arg ist gl arg =
then keep,ElimOnIdent (loc,id')
else
(keep, ElimOnConstr { delayed = begin fun env sigma ->
- try Sigma.here (EConstr.of_constr (constr_of_id env id'), NoBindings) sigma
+ try Sigma.here (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.")
@@ -1075,7 +1066,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 ((EConstr.of_constr c,NoBindings), sigma, Sigma.refl) }
+ | Some c -> keep,ElimOnConstr { delayed = fun env sigma -> Sigma ((c,NoBindings), sigma, Sigma.refl) }
with Not_found ->
(* We were in non strict (interactive) mode *)
if Tactics.is_quantified_hypothesis id gl then
@@ -1085,7 +1076,6 @@ 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
@@ -1365,7 +1355,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
Ftactic.s_enter { s_enter = begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
- let c = interp_uconstr ist env c in
+ let c = interp_uconstr ist env (Sigma.to_evar_map sigma) c in
let Sigma (c, sigma, p) = (type_uconstr ist c).delayed env sigma in
Sigma (Ftactic.return (Value.of_constr c), sigma, p)
end }
@@ -1468,7 +1458,7 @@ and interp_letin ist llc u =
and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
let (>>=) = Ftactic.bind in
let lctxt = Id.Map.map interp_context context in
- let hyp_subst = Id.Map.map (EConstr.Unsafe.to_constr %> Value.of_constr) terms in
+ let hyp_subst = Id.Map.map Value.of_constr terms in
let lfun = extend_values_with_bindings subst (lctxt +++ hyp_subst +++ ist.lfun) in
let ist = { ist with lfun } in
val_interp ist lhs >>= fun v ->
@@ -1522,7 +1512,6 @@ and interp_match ist lz constr lmr =
Proofview.tclZERO ~info e
end
end >>= fun constr ->
- let constr = EConstr.of_constr constr in
Ftactic.enter { enter = begin fun gl ->
let sigma = project gl in
let env = Proofview.Goal.env gl in
@@ -1597,7 +1586,7 @@ and interp_genarg_var_list ist x =
end }
(* Interprets tactic expressions : returns a "constr" *)
-and interp_ltac_constr ist e : constr Ftactic.t =
+and interp_ltac_constr ist e : EConstr.t Ftactic.t =
let (>>=) = Ftactic.bind in
begin Proofview.tclORELSE
(val_interp ist e)
@@ -1625,7 +1614,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
debugging_step ist (fun () ->
Pptactic.pr_glob_tactic env e ++ fnl() ++
str " has value " ++ fnl() ++
- pr_constr_env env sigma cresult)
+ pr_econstr_env env sigma cresult)
end <*>
Ftactic.return cresult
with CannotCoerceTo _ ->
@@ -1645,7 +1634,8 @@ and name_atomic ?env tacexpr tac : unit Proofview.tactic =
| Some e -> Proofview.tclUNIT e
| None -> Proofview.tclENV
end >>= fun env ->
- let name () = Pptactic.pr_atomic_tactic env tacexpr in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ let name () = Pptactic.pr_atomic_tactic env sigma tacexpr in
Proofview.Trace.name_tactic name tac
(* Interprets a primitive tactic *)
@@ -1712,7 +1702,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,EConstr.of_constr c_interp) in
+ sigma , (interp_ident ist env sigma id,n,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
@@ -1727,7 +1717,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,EConstr.of_constr c_interp) in
+ sigma , (interp_ident ist env sigma id,c_interp) in
let (sigma,l_interp) =
Evd.MonadR.List.map_right (fun c sigma -> f sigma c) l (project gl)
in
@@ -1742,7 +1732,6 @@ 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
@@ -1770,7 +1759,6 @@ 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
@@ -1789,7 +1777,6 @@ 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"*)
@@ -1849,7 +1836,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
in
let c_interp patvars = { Sigma.run = begin fun sigma ->
let lfun' = Id.Map.fold (fun id c lfun ->
- Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun)
+ Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
let sigma = Sigma.to_evar_map sigma in
@@ -1859,7 +1846,6 @@ 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)
@@ -1876,14 +1862,13 @@ and interp_atomic ist tac : unit Proofview.tactic =
let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
let c_interp patvars = { Sigma.run = begin fun sigma ->
let lfun' = Id.Map.fold (fun id c lfun ->
- Id.Map.add id (Value.of_constr (EConstr.Unsafe.to_constr c)) lfun)
+ Id.Map.add id (Value.of_constr c) lfun)
patvars ist.lfun
in
let ist = { ist with lfun = lfun' } in
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.")
@@ -1922,7 +1907,6 @@ 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
@@ -1949,7 +1933,6 @@ 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
@@ -2059,7 +2042,6 @@ 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)
}
@@ -2099,7 +2081,7 @@ let () =
let () =
register_interp0 wit_uconstr (fun ist c -> Ftactic.nf_enter { enter = begin fun gl ->
- Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) c)
+ Ftactic.return (interp_uconstr ist (Proofview.Goal.env gl) (Tacmach.New.project gl) c)
end })
(***************************************************************************)
diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli
index 2b0324e24..c657a11f1 100644
--- a/ltac/tacinterp.mli
+++ b/ltac/tacinterp.mli
@@ -9,6 +9,7 @@
open Names
open Tactic_debug
open Term
+open EConstr
open Tacexpr
open Genarg
open Redexpr
diff --git a/ltac/tactic_debug.ml b/ltac/tactic_debug.ml
index be1123d5c..b2601ad32 100644
--- a/ltac/tactic_debug.ml
+++ b/ltac/tactic_debug.ml
@@ -51,8 +51,7 @@ let db_pr_goal gl =
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let penv = print_named_context env in
- let concl = EConstr.Unsafe.to_constr concl in
- let pc = print_constr_env env concl in
+ let pc = print_constr_env env (Tacmach.New.project gl) concl in
str" " ++ hv 0 (penv ++ fnl () ++
str "============================" ++ fnl () ++
str" " ++ pc) ++ fnl ()
@@ -224,11 +223,11 @@ let is_debug db =
return (Int.equal skip 0)
(* Prints a constr *)
-let db_constr debug env c =
+let db_constr debug env sigma c =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
- msg_tac_debug (str "Evaluated term: " ++ print_constr_env env c)
+ msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c)
else return ()
(* Prints the pattern rule *)
@@ -248,20 +247,20 @@ let hyp_bound = function
| Name id -> str " (bound to " ++ pr_id id ++ str ")"
(* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,_,c) ido =
+let db_matched_hyp debug env sigma (id,_,c) ido =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
- str " has been matched: " ++ print_constr_env env c)
+ str " has been matched: " ++ print_constr_env env sigma c)
else return ()
(* Prints the matched conclusion *)
-let db_matched_concl debug env c =
+let db_matched_concl debug env sigma c =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
- msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env c)
+ msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c)
else return ()
(* Prints a success message when the goal has been matched *)
diff --git a/ltac/tactic_debug.mli b/ltac/tactic_debug.mli
index 520fb41ef..7745d9b7b 100644
--- a/ltac/tactic_debug.mli
+++ b/ltac/tactic_debug.mli
@@ -11,6 +11,7 @@ open Pattern
open Names
open Tacexpr
open Term
+open EConstr
open Evd
(** TODO: Move those definitions somewhere sensible *)
@@ -34,7 +35,7 @@ val debug_prompt :
val db_initialize : unit Proofview.NonLogical.t
(** Prints a constr *)
-val db_constr : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
(** Prints the pattern rule *)
val db_pattern_rule :
@@ -42,10 +43,10 @@ val db_pattern_rule :
(** Prints a matched hypothesis *)
val db_matched_hyp :
- debug_info -> env -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
+ debug_info -> env -> evar_map -> Id.t * constr option * constr -> Name.t -> unit Proofview.NonLogical.t
(** Prints the matched conclusion *)
-val db_matched_concl : debug_info -> env -> constr -> unit Proofview.NonLogical.t
+val db_matched_concl : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLogical.t
(** Prints a success message when the goal has been matched *)
val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
diff --git a/ltac/tauto.ml b/ltac/tauto.ml
index a4faf438a..707154a30 100644
--- a/ltac/tauto.ml
+++ b/ltac/tauto.ml
@@ -25,7 +25,7 @@ let () = Mltop.add_known_module tauto_plugin
let assoc_var s ist =
let v = Id.Map.find (Names.Id.of_string s) ist.lfun in
match Value.to_constr v with
- | Some c -> EConstr.of_constr c
+ | Some c -> c
| None -> failwith "tauto: anomaly"
(** Parametrization of tauto *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:12:30 +0000