aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extraargs.mlg31
-rw-r--r--plugins/ltac/extraargs.mli5
-rw-r--r--plugins/ltac/extratactics.mlg18
-rw-r--r--plugins/ltac/g_auto.mlg17
-rw-r--r--plugins/ltac/g_ltac.mlg41
-rw-r--r--plugins/ltac/g_obligations.mlg20
-rw-r--r--plugins/ltac/g_rewrite.mlg95
-rw-r--r--plugins/ltac/pptactic.ml292
-rw-r--r--plugins/ltac/pptactic.mli75
-rw-r--r--plugins/ltac/rewrite.ml125
-rw-r--r--plugins/ltac/rewrite.mli14
-rw-r--r--plugins/ltac/tacinterp.ml75
-rw-r--r--plugins/ltac/tacinterp.mli7
-rw-r--r--plugins/ltac/tactic_debug.ml15
-rw-r--r--plugins/ltac/tactic_debug.mli2
15 files changed, 435 insertions, 397 deletions
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index 5d5d45c58f..eb9cacb975 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -145,31 +145,30 @@ END
let pr_occurrences = pr_occurrences () () ()
-let pr_gen prc _prlc _prtac c = prc c
+let pr_gen env sigma prc _prlc _prtac x = prc env sigma x
-let pr_globc _prc _prlc _prtac (_,glob) =
- let _, env = Pfedit.get_current_context () in
+let pr_globc env sigma _prc _prlc _prtac (_,glob) =
Printer.pr_glob_constr_env env glob
let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t)
let glob_glob = Tacintern.intern_constr
-let pr_lconstr _ prc _ c = prc c
+let pr_lconstr env sigma _ prc _ c = prc env sigma c
let subst_glob = Tacsubst.subst_glob_constr_and_expr
}
ARGUMENT EXTEND glob
- PRINTED BY { pr_globc }
+ PRINTED BY { pr_globc env sigma }
INTERPRETED BY { interp_glob }
GLOBALIZED BY { glob_glob }
SUBSTITUTED BY { subst_glob }
- RAW_PRINTED BY { pr_gen }
- GLOB_PRINTED BY { pr_gen }
+ RAW_PRINTED BY { pr_gen env sigma }
+ GLOB_PRINTED BY { pr_gen env sigma }
| [ constr(c) ] -> { c }
END
@@ -181,20 +180,20 @@ let l_constr = Pcoq.Constr.lconstr
ARGUMENT EXTEND lconstr
TYPED AS constr
- PRINTED BY { pr_lconstr }
+ PRINTED BY { pr_lconstr env sigma }
| [ l_constr(c) ] -> { c }
END
ARGUMENT EXTEND lglob
TYPED AS glob
- PRINTED BY { pr_globc }
+ PRINTED BY { pr_globc env sigma }
INTERPRETED BY { interp_glob }
GLOBALIZED BY { glob_glob }
SUBSTITUTED BY { subst_glob }
- RAW_PRINTED BY { pr_gen }
- GLOB_PRINTED BY { pr_gen }
+ RAW_PRINTED BY { pr_gen env sigma }
+ GLOB_PRINTED BY { pr_gen env sigma }
| [ lconstr(c) ] -> { c }
END
@@ -207,7 +206,7 @@ let interp_casted_constr ist gl c =
ARGUMENT EXTEND casted_constr
TYPED AS constr
- PRINTED BY { pr_gen }
+ PRINTED BY { pr_gen env sigma }
INTERPRETED BY { interp_casted_constr }
| [ constr(c) ] -> { c }
END
@@ -296,23 +295,23 @@ END
{
-let pr_by_arg_tac _prc _prlc prtac opt_c =
+let pr_by_arg_tac env sigma _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac env sigma (3,Notation_gram.E) t)
}
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic option
- PRINTED BY { pr_by_arg_tac }
+ PRINTED BY { pr_by_arg_tac env sigma }
| [ "by" tactic3(c) ] -> { Some c }
| [ ] -> { None }
END
{
-let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c
+let pr_by_arg_tac env sigma prtac opt_c = pr_by_arg_tac env sigma () () prtac opt_c
let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Pputils.pr_lident cl
let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 0509d6ae71..7f9eecbef5 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -65,8 +65,9 @@ val wit_by_arg_tac :
glob_tactic_expr option,
Geninterp.Val.t option) Genarg.genarg_type
-val pr_by_arg_tac :
- (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
+val pr_by_arg_tac :
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Entry.t
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0428f08138..f5098d2a34 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -53,6 +53,7 @@ let with_delayed_uconstr ist c tac =
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
} in
let c = Tacinterp.type_uconstr ~flags ist c in
Tacticals.New.tclDELAYEDWITHHOLES false c tac
@@ -348,6 +349,7 @@ let constr_flags () = {
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
+ Pretyping.polymorphic = false;
}
let refine_tac ist simple with_classes c =
@@ -813,9 +815,9 @@ END
TACTIC EXTEND transparent_abstract
| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl ->
- Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end }
+ Abstract.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end; }
| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl ->
- Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end }
+ Abstract.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end; }
END
(* ********************************************************************* *)
@@ -913,9 +915,9 @@ END
the semantics of the LCF-style tactics, hence with the classic tactic
mode. *)
VERNAC COMMAND EXTEND GrabEvars
-| [ "Grab" "Existential" "Variables" ]
+| ![ proof ] [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) }
+ -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate }
END
(* Shelves all the goals under focus. *)
@@ -945,9 +947,9 @@ END
(* Command to add every unshelved variables to the focus *)
VERNAC COMMAND EXTEND Unshelve
-| [ "Unshelve" ]
+| ![ proof ] [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) }
+ -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
@@ -1098,8 +1100,8 @@ END
VERNAC COMMAND EXTEND OptimizeProof
-| [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { Proof_global.compact_the_proof () }
+| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
+ { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 663537f3e8..523c7c8305 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -58,25 +58,24 @@ let eval_uconstrs ist cs =
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
} in
let map c env sigma = c env sigma in
List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs
-let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr
-let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
- let _, env = Pfedit.get_current_context () in
+let pr_auto_using_raw env sigma _ _ _ = Pptactic.pr_auto_using @@ Ppconstr.pr_constr_expr env sigma
+let pr_auto_using_glob env sigma _ _ _ = Pptactic.pr_auto_using (fun (c,_) ->
Printer.pr_glob_constr_env env c)
-let pr_auto_using _ _ _ = Pptactic.pr_auto_using
- (let sigma, env = Pfedit.get_current_context () in
- Printer.pr_closed_glob_env env sigma)
+let pr_auto_using env sigma _ _ _ = Pptactic.pr_auto_using @@
+ Printer.pr_closed_glob_env env sigma
}
ARGUMENT EXTEND auto_using
TYPED AS uconstr list
- PRINTED BY { pr_auto_using }
- RAW_PRINTED BY { pr_auto_using_raw }
- GLOB_PRINTED BY { pr_auto_using_glob }
+ PRINTED BY { pr_auto_using env sigma }
+ RAW_PRINTED BY { pr_auto_using_raw env sigma }
+ GLOB_PRINTED BY { pr_auto_using_glob env sigma }
| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l }
| [ ] -> { [] }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 4c24f51b1e..7eb34158e8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -374,20 +374,21 @@ let () = declare_int_option {
optwrite = fun n -> print_info_trace := n;
}
-let vernac_solve n info tcom b =
+let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let status = Proof_global.with_current_proof (fun etac p ->
- let with_end_tac = if b then Some etac else None in
- let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info !print_info_trace in
- let (p,status) =
- Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
- in
- (* in case a strict subtree was completed,
- go back to the top of the prooftree *)
- let p = Proof.maximal_unfocus Vernacentries.command_focus p in
- p,status) in
- if not status then Feedback.feedback Feedback.AddedAxiom
+ let pstate, status = Proof_global.with_current_proof (fun etac p ->
+ let with_end_tac = if b then Some etac else None in
+ let global = match n with SelectAll | SelectList _ -> true | _ -> false in
+ let info = Option.append info !print_info_trace in
+ let (p,status) =
+ Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+ in
+ (* in case a strict subtree was completed,
+ go back to the top of the prooftree *)
+ let p = Proof.maximal_unfocus Vernacentries.command_focus p in
+ p,status) pstate in
+ if not status then Feedback.feedback Feedback.AddedAxiom;
+ Some pstate
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
@@ -434,12 +435,12 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
VERNAC { tactic_mode } EXTEND VernacSolve
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- vernac_solve g n t def
+ Vernacentries.vernac_require_open_proof vernac_solve g n t def
}
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{
let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
@@ -449,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
VtLater
} -> {
let t = rm_abstract t in
- vernac_solve Goal_select.SelectAll n t def
+ Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
}
END
@@ -514,7 +515,7 @@ END
let pr_ltac_ref = Libnames.pr_qualid
-let pr_tacdef_body tacdef_body =
+let pr_tacdef_body env sigma tacdef_body =
let id, redef, body =
match tacdef_body with
| TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body
@@ -528,12 +529,12 @@ let pr_tacdef_body tacdef_body =
prlist (function Name.Anonymous -> str " _"
| Name.Name id -> spc () ++ Id.print id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
- ++ Pptactic.pr_raw_tactic body
+ ++ Pptactic.pr_raw_tactic env sigma body
}
VERNAC ARGUMENT EXTEND ltac_tacdef_body
-PRINTED BY { pr_tacdef_body }
+PRINTED BY { pr_tacdef_body env sigma }
| [ tacdef_body(t) ] -> { t }
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index cdee012a82..de3a9c9fa9 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
open Obligations
-let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
-let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
+let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
+let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
-| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
-| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
@@ -162,9 +162,9 @@ END
(* Declare a printer for the content of Program tactics *)
let () =
- let printer _ _ _ = function
+ let printer env sigma _ _ _ = function
| None -> mt ()
- | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac
+ | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic env sigma tac
in
Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index db8d1b20d8..469551809c 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -41,13 +41,11 @@ type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = glob_constr_and_expr with_bindings
type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
-let pr_glob_constr_with_bindings_sign _ _ _ (ge : glob_constr_with_bindings_sign) =
- let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
Printer.pr_glob_constr_env env (fst (fst (snd ge)))
-let pr_glob_constr_with_bindings _ _ _ (ge : glob_constr_with_bindings) =
- let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
Printer.pr_glob_constr_env env (fst (fst ge))
-let pr_constr_expr_with_bindings prc _ _ (ge : constr_expr_with_bindings) = prc (fst ge)
+let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
let interp_glob_constr_with_bindings ist gl c = Tacmach.project gl , (ist, c)
let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
let subst_glob_constr_with_bindings s c =
@@ -56,14 +54,14 @@ let subst_glob_constr_with_bindings s c =
}
ARGUMENT EXTEND glob_constr_with_bindings
- PRINTED BY { pr_glob_constr_with_bindings_sign }
+ PRINTED BY { pr_glob_constr_with_bindings_sign env sigma }
INTERPRETED BY { interp_glob_constr_with_bindings }
GLOBALIZED BY { glob_glob_constr_with_bindings }
SUBSTITUTED BY { subst_glob_constr_with_bindings }
- RAW_PRINTED BY { pr_constr_expr_with_bindings }
- GLOB_PRINTED BY { pr_glob_constr_with_bindings }
+ RAW_PRINTED BY { pr_constr_expr_with_bindings env sigma }
+ GLOB_PRINTED BY { pr_glob_constr_with_bindings env sigma }
| [ constr_with_bindings(bl) ] -> { bl }
END
@@ -80,17 +78,17 @@ let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c
let subst_strategy s str = str
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
-let pr_raw_strategy prc prlc _ (s : raw_strategy) =
- let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
- Rewrite.pr_strategy prc prr s
-let pr_glob_strategy prc prlc _ (s : glob_strategy) =
- let prr = Pptactic.pr_red_expr
+let pr_raw_strategy env sigma prc prlc _ (s : raw_strategy) =
+ let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in
+ Rewrite.pr_strategy (prc env sigma) prr s
+let pr_glob_strategy env sigma prc prlc _ (s : glob_strategy) =
+ let prr = Pptactic.pr_red_expr env sigma
(Ppconstr.pr_constr_expr,
Ppconstr.pr_lconstr_expr,
Pputils.pr_or_by_notation Libnames.pr_qualid,
Ppconstr.pr_constr_expr)
in
- Rewrite.pr_strategy prc prr s
+ Rewrite.pr_strategy (prc env sigma) prr s
}
@@ -101,8 +99,8 @@ ARGUMENT EXTEND rewstrategy
GLOBALIZED BY { glob_strategy }
SUBSTITUTED BY { subst_strategy }
- RAW_PRINTED BY { pr_raw_strategy }
- GLOB_PRINTED BY { pr_glob_strategy }
+ RAW_PRINTED BY { pr_raw_strategy env sigma }
+ GLOB_PRINTED BY { pr_glob_strategy env sigma }
| [ glob(c) ] -> { StratConstr (c, true) }
| [ "<-" constr(c) ] -> { StratConstr (c, false) }
@@ -182,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
{ declare_relation atts a aeq n None None None }
END
VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts a aeq n None None (Some lemma3) }
END
@@ -224,7 +222,7 @@ let wit_binders =
let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
let () =
- let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in
+ let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer
}
@@ -236,64 +234,64 @@ GRAMMAR EXTEND Gram
END
VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None None }
END
VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
END
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid atts [] a aeq t n;
+ add_setoid atts [] a aeq t n
}
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
- add_setoid atts binders a aeq t n;
+ add_setoid atts binders a aeq t n
}
- | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
=> { VtUnknown, VtNow }
-> {
- add_morphism_infer atts m n;
+ add_morphism_infer atts m n
}
- | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
- add_morphism atts [] m s n;
+ add_morphism atts [] m s n
}
- | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+ | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
=> { VtStartProof(GuaranteesOpacity,[n]), VtLater }
-> {
- add_morphism atts binders m s n;
+ add_morphism atts binders m s n
}
END
@@ -312,7 +310,12 @@ TACTIC EXTEND setoid_transitivity
END
VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
- { let sigma, env = Pfedit.get_current_context () in
- Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) }
+| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+ { (* This command should not use the proof env, keeping previous
+ behavior as requested in review. *)
+ fun ~pstate ->
+ let sigma, env = Option.cata Pfedit.get_current_context
+ (let e = Global.env () in Evd.from_env e, e) pstate in
+ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s);
+ pstate }
END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index e188971f00..80070a7493 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -71,40 +71,46 @@ let declare_notation_tactic_pprule kn pt =
prnotation_tab := KNmap.add kn pt !prnotation_tab
type 'a raw_extra_genarg_printer =
- (constr_expr -> Pp.t) ->
- (constr_expr -> Pp.t) ->
- (tolerability -> raw_tactic_expr -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> Pp.t) ->
- (glob_constr_and_expr -> Pp.t) ->
- (tolerability -> glob_tactic_expr -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a extra_genarg_printer =
- (EConstr.constr -> Pp.t) ->
- (EConstr.constr -> Pp.t) ->
- (tolerability -> Val.t -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ 'a -> Pp.t
type 'a raw_extra_genarg_printer_with_level =
- (constr_expr -> Pp.t) ->
- (constr_expr -> Pp.t) ->
- (tolerability -> raw_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
type 'a glob_extra_genarg_printer_with_level =
- (glob_constr_and_expr -> Pp.t) ->
- (glob_constr_and_expr -> Pp.t) ->
- (tolerability -> glob_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
type 'a extra_genarg_printer_with_level =
- (EConstr.constr -> Pp.t) ->
- (EConstr.constr -> Pp.t) ->
- (tolerability -> Val.t -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
let string_of_genarg_arg (ArgumentType arg) =
let rec aux : type a b c. (a, b, c) genarg_type -> string = function
@@ -160,27 +166,27 @@ let string_of_genarg_arg (ArgumentType arg) =
| _ -> default
let pr_with_occurrences pr c = Ppred.pr_with_occurrences pr keyword c
- let pr_red_expr pr c = Ppred.pr_red_expr pr keyword c
+ let pr_red_expr env sigma pr c = Ppred.pr_red_expr_env env sigma pr keyword c
- let pr_may_eval test prc prlc pr2 pr3 = function
+ let pr_may_eval env sigma test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
hov 0
(keyword "eval" ++ brk (1,1) ++
- pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++
- keyword "in" ++ spc() ++ prc c)
+ pr_red_expr env sigma (prc,prlc,pr2,pr3) r ++ spc () ++
+ keyword "in" ++ spc() ++ prc env sigma c)
| ConstrContext ({CAst.v=id},c) ->
hov 0
(keyword "context" ++ spc () ++ pr_id id ++ spc () ++
- str "[ " ++ prlc c ++ str " ]")
+ str "[ " ++ prlc env sigma c ++ str " ]")
| ConstrTypeOf c ->
- hov 1 (keyword "type of" ++ spc() ++ prc c)
+ hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc c ++ str ")")
+ h 0 (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
- prc c
+ prc env sigma c
- let pr_may_eval a =
- pr_may_eval (fun _ -> false) a
+ let pr_may_eval env sigma a =
+ pr_may_eval env sigma (fun _ -> false) a
let pr_arg pr x = spc () ++ pr x
@@ -647,15 +653,15 @@ let pr_goal_selector ~toplevel s =
type 'a printer = {
pr_tactic : tolerability -> 'tacexpr -> Pp.t;
- pr_constr : 'trm -> Pp.t;
- pr_lconstr : 'trm -> Pp.t;
- pr_dconstr : 'dtrm -> Pp.t;
- pr_pattern : 'pat -> Pp.t;
- pr_lpattern : 'pat -> Pp.t;
+ pr_constr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
+ pr_lconstr : Environ.env -> Evd.evar_map -> 'trm -> Pp.t;
+ pr_dconstr : Environ.env -> Evd.evar_map -> 'dtrm -> Pp.t;
+ pr_pattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
+ pr_lpattern : Environ.env -> Evd.evar_map -> 'pat -> Pp.t;
pr_constant : 'cst -> Pp.t;
pr_reference : 'ref -> Pp.t;
pr_name : 'nam -> Pp.t;
- pr_generic : 'lev generic_argument -> Pp.t;
+ pr_generic : Environ.env -> Evd.evar_map -> 'lev generic_argument -> Pp.t;
pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t;
pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t;
}
@@ -671,14 +677,14 @@ let pr_goal_selector ~toplevel s =
level :'lev
>
- let pr_atom pr strip_prod_binders tag_atom =
- let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in
+ let pr_atom env sigma pr strip_prod_binders tag_atom =
+ let pr_with_bindings = pr_with_bindings (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
let pr_with_bindings_arg_full = pr_with_bindings_arg in
- let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
- let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
+ let pr_with_bindings_arg = pr_with_bindings_arg (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) in
+ let pr_red_expr = pr_red_expr env sigma (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
- let _pr_constrarg c = spc () ++ pr.pr_constr c in
- let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
+ let _pr_constrarg c = spc () ++ pr.pr_constr env sigma c in
+ let pr_lconstrarg c = spc () ++ pr.pr_lconstr env sigma c in
let pr_intarg n = spc () ++ int n in
(* Some printing combinators *)
@@ -688,7 +694,7 @@ let pr_goal_selector ~toplevel s =
(* match t with
| CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal
| _ ->*)
- let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in
+ let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr env sigma t in
spc() ++ hov 1 (str"(" ++ s ++ str")") in
let pr_fix_tac (id,n,c) =
@@ -723,7 +729,7 @@ let pr_goal_selector ~toplevel s =
in
hov 1 (str"(" ++ pr_id id ++
prlist pr_binder_fix bll ++ annot ++ str" :" ++
- pr_lconstrarg ty ++ str")") in
+ (pr_lconstrarg ty) ++ str")") in
(* spc() ++
hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
c)
@@ -747,13 +753,13 @@ let pr_goal_selector ~toplevel s =
hov 1 (primitive (if ev then "eintros" else "intros") ++
(match p with
| [{CAst.v=IntroForthcoming false}] -> mt ()
- | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p))
+ | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern @@ pr.pr_dconstr env sigma) p))
| TacApply (a,ev,cb,inhyp) ->
hov 1 (
(if a then mt() else primitive "simple ") ++
primitive (with_evars ev "apply") ++ spc () ++
prlist_with_sep pr_comma pr_with_bindings_arg cb ++
- pr_non_empty_arg (pr_in_hyp_as pr.pr_dconstr pr.pr_name) inhyp
+ pr_non_empty_arg (pr_in_hyp_as (pr.pr_dconstr env sigma) pr.pr_name) inhyp
)
| TacElim (ev,cb,cbo) ->
hov 1 (
@@ -774,28 +780,28 @@ let pr_goal_selector ~toplevel s =
| TacAssert (ev,b,Some tac,ipat,c) ->
hov 1 (
primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
- pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
+ pr_assumption (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c ++
pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
)
| TacAssert (ev,_,None,ipat,c) ->
hov 1 (
primitive (if ev then "epose proof" else "pose proof")
- ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
+ ++ pr_assertion (pr.pr_constr env sigma) (pr.pr_dconstr env sigma) (pr.pr_lconstr env sigma) ipat c
)
| TacGeneralize l ->
hov 1 (
primitive "generalize" ++ spc ()
++ prlist_with_sep pr_comma (fun (cl,na) ->
- pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
+ pr_with_occurrences (pr.pr_constr env sigma) cl ++ pr_as_name na)
l
)
| TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
- hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+ hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c)
| TacLetTac (ev,na,c,cl,b,e) ->
hov 1 (
primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
- (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
- else pr_pose_as_style pr.pr_constr na c) ++
+ (if b then pr_pose (pr.pr_constr env sigma) (pr.pr_lconstr env sigma) na c
+ else pr_pose_as_style (pr.pr_constr env sigma) na c) ++
pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
pr_non_empty_arg (pr_clauses (Some b) pr.pr_name) cl)
(* | TacInstantiate (n,c,ConclLocation ()) ->
@@ -815,8 +821,8 @@ let pr_goal_selector ~toplevel s =
primitive (with_evars ev (if isrec then "induction" else "destruct"))
++ spc ()
++ prlist_with_sep pr_comma (fun (h,ids,cl) ->
- pr_destruction_arg pr.pr_dconstr pr.pr_dconstr h ++
- pr_non_empty_arg (pr_with_induction_names pr.pr_dconstr) ids ++
+ pr_destruction_arg (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) h ++
+ pr_non_empty_arg (pr_with_induction_names (pr.pr_dconstr env sigma)) ids ++
pr_opt (pr_clauses None pr.pr_name) cl) l ++
pr_opt pr_eliminator el
)
@@ -835,9 +841,9 @@ let pr_goal_selector ~toplevel s =
None ->
mt ()
| Some p ->
- pr.pr_pattern p ++ spc ()
+ pr.pr_pattern env sigma p ++ spc ()
++ keyword "with" ++ spc ()
- ) ++ pr.pr_dconstr c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
+ ) ++ pr.pr_dconstr env sigma c ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
(* Equality and inversion *)
@@ -848,7 +854,7 @@ let pr_goal_selector ~toplevel s =
(fun () -> str ","++spc())
(fun (b,m,c) ->
pr_orient b ++ pr_multi m ++
- pr_with_bindings_arg_full pr.pr_dconstr pr.pr_dconstr c)
+ pr_with_bindings_arg_full (pr.pr_dconstr env sigma) (pr.pr_dconstr env sigma) c)
l
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) cl
++ pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
@@ -857,28 +863,28 @@ let pr_goal_selector ~toplevel s =
hov 1 (
primitive "dependent " ++ pr_inversion_kind k ++ spc ()
++ pr_quantified_hypothesis hyp
- ++ pr_with_inversion_names pr.pr_dconstr ids
- ++ pr_with_constr pr.pr_constr c
+ ++ pr_with_inversion_names (pr.pr_dconstr env sigma) ids
+ ++ pr_with_constr (pr.pr_constr env sigma) c
)
| TacInversion (NonDepInversion (k,cl,ids),hyp) ->
hov 1 (
pr_inversion_kind k ++ spc ()
++ pr_quantified_hypothesis hyp
- ++ pr_non_empty_arg (pr_with_inversion_names pr.pr_dconstr) ids
+ ++ pr_non_empty_arg (pr_with_inversion_names @@ pr.pr_dconstr env sigma) ids
++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
)
| TacInversion (InversionUsing (c,cl),hyp) ->
hov 1 (
primitive "inversion" ++ spc()
++ pr_quantified_hypothesis hyp ++ spc ()
- ++ keyword "using" ++ spc () ++ pr.pr_constr c
+ ++ keyword "using" ++ spc () ++ pr.pr_constr env sigma c
++ pr_non_empty_arg (pr_simple_hyp_clause pr.pr_name) cl
)
)
in
pr_atom1
- let make_pr_tac pr strip_prod_binders tag_atom tag =
+ let make_pr_tac env sigma pr strip_prod_binders tag_atom tag =
let extract_binders = function
| Tacexp (TacFun (lvar,body)) -> (lvar,Tacexp body)
@@ -898,7 +904,7 @@ let pr_goal_selector ~toplevel s =
let llc = List.map (fun (id,t) -> (id,extract_binders t)) llc in
v 0
(hv 0 (
- pr_let_clauses recflag pr.pr_generic (pr_tac ltop) llc
+ pr_let_clauses recflag (pr.pr_generic env sigma) (pr_tac ltop) llc
++ spc () ++ keyword "in"
) ++ fnl () ++ pr_tac (llet,E) u),
llet
@@ -908,7 +914,7 @@ let pr_goal_selector ~toplevel s =
++ pr_tac ltop t ++ spc () ++ keyword "with"
++ prlist (fun r ->
fnl () ++ str "| "
- ++ pr_match_rule true (pr_tac ltop) pr.pr_lpattern r
+ ++ pr_match_rule true (pr_tac ltop) (pr.pr_lpattern env sigma) r
) lrul
++ fnl() ++ keyword "end"),
lmatch
@@ -918,7 +924,7 @@ let pr_goal_selector ~toplevel s =
++ keyword (if lr then "match reverse goal with" else "match goal with")
++ prlist (fun r ->
fnl () ++ str "| "
- ++ pr_match_rule false (pr_tac ltop) pr.pr_lpattern r
+ ++ pr_match_rule false (pr_tac ltop) (pr.pr_lpattern env sigma) r
) lrul ++ fnl() ++ keyword "end"),
lmatch
| TacFun (lvar,body) ->
@@ -1041,17 +1047,17 @@ let pr_goal_selector ~toplevel s =
| TacId l ->
keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
| TacAtom { CAst.loc; v=t } ->
- pr_with_comments ?loc (hov 1 (pr_atom pr strip_prod_binders tag_atom t)), ltatom
+ pr_with_comments ?loc (hov 1 (pr_atom env sigma pr strip_prod_binders tag_atom t)), ltatom
| TacArg { CAst.v=Tacexp e } ->
pr_tac inherited e, latom
| TacArg { CAst.v=ConstrMayEval (ConstrTerm c) } ->
- keyword "constr:" ++ pr.pr_constr c, latom
+ keyword "constr:" ++ pr.pr_constr env sigma c, latom
| TacArg { CAst.v=ConstrMayEval c } ->
- pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
+ pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c, leval
| TacArg { CAst.v=TacFreshId l } ->
primitive "fresh" ++ pr_fresh_ids l, latom
| TacArg { CAst.v=TacGeneric arg } ->
- pr.pr_generic arg, latom
+ pr.pr_generic env sigma arg, latom
| TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
| TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
@@ -1074,11 +1080,11 @@ let pr_goal_selector ~toplevel s =
| Reference r ->
pr.pr_reference r
| ConstrMayEval c ->
- pr_may_eval pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
+ pr_may_eval env sigma pr.pr_constr pr.pr_lconstr pr.pr_constant pr.pr_pattern c
| TacFreshId l ->
keyword "fresh" ++ pr_fresh_ids l
| TacPretype c ->
- keyword "type_term" ++ pr.pr_constr c
+ keyword "type_term" ++ pr.pr_constr env sigma c
| TacNumgoals ->
keyword "numgoals"
| (TacCall _|Tacexp _ | TacGeneric _) as a ->
@@ -1098,9 +1104,9 @@ let pr_goal_selector ~toplevel s =
let raw_printers =
(strip_prod_binders_expr)
- let rec pr_raw_tactic_level n (t:raw_tactic_expr) =
+ let rec pr_raw_tactic_level env sigma n (t:raw_tactic_expr) =
let pr = {
- pr_tactic = pr_raw_tactic_level;
+ pr_tactic = pr_raw_tactic_level env sigma;
pr_constr = pr_constr_expr;
pr_dconstr = pr_constr_expr;
pr_lconstr = pr_lconstr_expr;
@@ -1109,16 +1115,16 @@ let pr_goal_selector ~toplevel s =
pr_constant = pr_or_by_notation pr_qualid;
pr_reference = pr_qualid;
pr_name = pr_lident;
- pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg);
- pr_extend = pr_raw_extend_rec pr_raw_tactic_level;
- pr_alias = pr_raw_alias pr_raw_tactic_level;
+ pr_generic = Pputils.pr_raw_generic;
+ pr_extend = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma;
+ pr_alias = pr_raw_alias @@ pr_raw_tactic_level env sigma;
} in
- make_pr_tac
+ make_pr_tac env sigma
pr raw_printers
tag_raw_atomic_tactic_expr tag_raw_tactic_expr
n t
- let pr_raw_tactic = pr_raw_tactic_level ltop
+ let pr_raw_tactic env sigma = pr_raw_tactic_level env sigma ltop
let pr_and_constr_expr pr (c,_) = pr c
@@ -1131,19 +1137,19 @@ let pr_goal_selector ~toplevel s =
let rec prtac n (t:glob_tactic_expr) =
let pr = {
pr_tactic = prtac;
- pr_constr = pr_and_constr_expr (pr_glob_constr_env env);
- pr_dconstr = pr_and_constr_expr (pr_glob_constr_env env);
- pr_lconstr = pr_and_constr_expr (pr_lglob_constr_env env);
- pr_pattern = pr_pat_and_constr_expr (pr_glob_constr_env env);
- pr_lpattern = pr_pat_and_constr_expr (pr_lglob_constr_env env);
+ pr_constr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+ pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+ pr_lconstr = (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env));
+ pr_pattern = (fun env sigma -> pr_pat_and_constr_expr (pr_glob_constr_env env));
+ pr_lpattern = (fun env sigma -> pr_pat_and_constr_expr (pr_lglob_constr_env env));
pr_constant = pr_or_var (pr_and_short_name (pr_evaluable_reference_env env));
pr_reference = pr_ltac_or_var (pr_located pr_ltac_constant);
pr_name = pr_lident;
- pr_generic = (fun arg -> Pputils.pr_glb_generic (Global.env ()) arg);
+ pr_generic = Pputils.pr_glb_generic;
pr_extend = pr_glob_extend_rec prtac;
pr_alias = pr_glob_alias prtac;
} in
- make_pr_tac
+ make_pr_tac env (Evd.from_env env)
pr glob_printers
tag_glob_atomic_tactic_expr tag_glob_tactic_expr
n t
@@ -1166,11 +1172,11 @@ let pr_goal_selector ~toplevel s =
let prtac (t:atomic_tactic_expr) =
let pr = {
pr_tactic = (fun _ _ -> str "<tactic>");
- 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_leconstr_env env sigma c);
- pr_pattern = pr_constr_pattern_env env sigma;
- pr_lpattern = pr_lconstr_pattern_env env sigma;
+ pr_constr = pr_econstr_env;
+ pr_dconstr = (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env));
+ pr_lconstr = pr_leconstr_env;
+ pr_pattern = pr_constr_pattern_env;
+ pr_lpattern = pr_lconstr_pattern_env;
pr_constant = pr_evaluable_reference_env env;
pr_reference = pr_located pr_ltac_constant;
pr_name = pr_id;
@@ -1180,7 +1186,7 @@ let pr_goal_selector ~toplevel s =
pr_alias = (fun _ _ _ -> assert false);
}
in
- pr_atom pr strip_prod_binders_constr tag_atomic_tactic_expr t
+ pr_atom env sigma pr strip_prod_binders_constr tag_atomic_tactic_expr t
in
prtac t
@@ -1188,9 +1194,9 @@ let pr_goal_selector ~toplevel s =
let pr_glb_generic = Pputils.pr_glb_generic
- let pr_raw_extend _ = pr_raw_extend_rec pr_raw_tactic_level
+ let pr_raw_extend env sigma = pr_raw_extend_rec @@ pr_raw_tactic_level env sigma
- let pr_glob_extend env = pr_glob_extend_rec (pr_glob_tactic_level env)
+ let pr_glob_extend env sigma = pr_glob_extend_rec (pr_glob_tactic_level env)
let pr_alias pr lev key args =
pr_alias_gen (fun _ arg -> pr arg) lev key args
@@ -1209,16 +1215,17 @@ let declare_extra_genarg_pprule wit
| _ -> user_err Pp.(str "Can declare a pretty-printing rule only for extra argument types.")
end;
let f x =
- Genprint.PrinterBasic (fun () ->
- f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
+ Genprint.PrinterBasic (fun env sigma ->
+ f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
let g x =
- Genprint.PrinterBasic (fun () ->
- let env = Global.env () in
- g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) x)
+ Genprint.PrinterBasic (fun env sigma ->
+ g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
+ (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+ (fun env sigma -> pr_glob_tactic_level env) x)
in
let h x =
Genprint.TopPrinterNeedsContext (fun env sigma ->
- h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") x)
+ h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") x)
in
Genprint.register_print0 wit f g h
@@ -1235,27 +1242,28 @@ let declare_extra_genarg_pprule_with_level wit
PrinterNeedsLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
- printer = (fun n ->
- f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
+ printer = (fun env sigma n ->
+ f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level n x) } in
let g x =
- let env = Global.env () in
PrinterNeedsLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
- printer = (fun n ->
- g (pr_and_constr_expr (pr_glob_constr_env env)) (pr_and_constr_expr (pr_lglob_constr_env env)) (pr_glob_tactic_level env) n x) }
+ printer = (fun env sigma n ->
+ g env sigma (fun env sigma -> pr_and_constr_expr (pr_glob_constr_env env))
+ (fun env sigma -> pr_and_constr_expr (pr_lglob_constr_env env))
+ (fun env sigma -> pr_glob_tactic_level env) n x) }
in
let h x =
TopPrinterNeedsContextAndLevel {
default_already_surrounded = default_surrounded;
default_ensure_surrounded = default_non_surrounded;
printer = (fun env sigma n ->
- h (pr_econstr_env env sigma) (pr_leconstr_env env sigma) (fun _ _ -> str "<tactic>") n x) }
+ h env sigma pr_econstr_env pr_leconstr_env (fun _env _sigma _ _ -> str "<tactic>") n x) }
in
Genprint.register_print0 wit f g h
let declare_extra_vernac_genarg_pprule wit f =
- let f x = Genprint.PrinterBasic (fun () -> f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
+ let f x = Genprint.PrinterBasic (fun env sigma -> f env sigma pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x) in
Genprint.register_vernac_print0 wit f
(** Registering *)
@@ -1265,8 +1273,8 @@ let pr_intro_pattern_env p = Genprint.TopPrinterNeedsContext (fun env sigma ->
Miscprint.pr_intro_pattern print_constr p)
let pr_red_expr_env r = Genprint.TopPrinterNeedsContext (fun env sigma ->
- pr_red_expr (pr_econstr_env env sigma, pr_leconstr_env env sigma,
- pr_evaluable_reference_env env, pr_constr_pattern_env env sigma) r)
+ pr_red_expr env sigma (pr_econstr_env, pr_leconstr_env,
+ pr_evaluable_reference_env env, pr_constr_pattern_env) r)
let pr_bindings_env bl = Genprint.TopPrinterNeedsContext (fun env sigma ->
let sigma, bl = bl env sigma in
@@ -1292,19 +1300,17 @@ let make_constr_printer f c =
Genprint.default_ensure_surrounded = Ppconstr.lsimpleconstr;
Genprint.printer = (fun env sigma n -> f env sigma n c)}
-let lift f a = Genprint.PrinterBasic (fun () -> f a)
+let lift f a = Genprint.PrinterBasic (fun env sigma -> f a)
+let lift_env f a = Genprint.PrinterBasic (fun env sigma -> f env sigma a)
let lift_top f a = Genprint.TopPrinterBasic (fun () -> f a)
let register_basic_print0 wit f g h =
Genprint.register_print0 wit (lift f) (lift g) (lift_top h)
-
-let pr_glob_constr_pptac c =
- let _, env = Pfedit.get_current_context () in
+let pr_glob_constr_pptac env sigma c =
pr_glob_constr_env env c
-let pr_lglob_constr_pptac c =
- let _, env = Pfedit.get_current_context () in
+let pr_lglob_constr_pptac env sigma c =
pr_lglob_constr_env env c
let () =
@@ -1318,8 +1324,8 @@ let () =
register_basic_print0 wit_var pr_lident pr_lident pr_id;
register_print0
wit_intro_pattern
- (lift (Miscprint.pr_intro_pattern pr_constr_expr))
- (lift (Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac c)))
+ (lift_env (fun env sigma -> Miscprint.pr_intro_pattern @@ pr_constr_expr env sigma))
+ (lift_env (fun env sigma -> Miscprint.pr_intro_pattern (fun (c,_) -> pr_glob_constr_pptac env sigma c)))
pr_intro_pattern_env;
Genprint.register_print0
wit_clause_dft_concl
@@ -1329,47 +1335,55 @@ let () =
;
Genprint.register_print0
wit_constr
- (lift Ppconstr.pr_lconstr_expr)
- (lift (fun (c, _) -> pr_lglob_constr_pptac c))
+ (lift_env Ppconstr.pr_lconstr_expr)
+ (lift_env (fun env sigma (c, _) -> pr_lglob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_uconstr
- (lift Ppconstr.pr_constr_expr)
- (lift (fun (c,_) -> pr_glob_constr_pptac c))
+ (lift_env Ppconstr.pr_constr_expr)
+ (lift_env (fun env sigma (c,_) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_closed_glob_n_env)
;
Genprint.register_print0
wit_open_constr
- (lift Ppconstr.pr_constr_expr)
- (lift (fun (c, _) -> pr_glob_constr_pptac c))
+ (lift_env Ppconstr.pr_constr_expr)
+ (lift_env (fun env sigma (c, _) -> pr_glob_constr_pptac env sigma c))
(make_constr_printer Printer.pr_econstr_n_env)
;
Genprint.register_print0
wit_red_expr
- (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
- (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac)))
+ (lift_env (fun env sigma -> pr_red_expr env sigma (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr)))
+ (lift_env (fun env sigma -> pr_red_expr env sigma
+ ((fun env sigma -> pr_and_constr_expr @@ pr_glob_constr_pptac env sigma),
+ (fun env sigma -> pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma),
+ pr_or_var (pr_and_short_name pr_evaluable_reference),
+ (fun env sigma -> pr_pat_and_constr_expr @@ pr_glob_constr_pptac env sigma))))
pr_red_expr_env
;
register_basic_print0 wit_quant_hyp pr_quantified_hypothesis pr_quantified_hypothesis pr_quantified_hypothesis;
register_print0 wit_bindings
- (lift (Miscprint.pr_bindings_no_with pr_constr_expr pr_lconstr_expr))
- (lift (Miscprint.pr_bindings_no_with (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+ (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_constr_expr env sigma)
+ (pr_lconstr_expr env sigma)))
+ (lift_env (fun env sigma -> Miscprint.pr_bindings_no_with (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma) (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_bindings_env
;
register_print0 wit_constr_with_bindings
- (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
- (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+ (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+ (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+ (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_with_bindings_env
;
register_print0 wit_open_constr_with_bindings
- (lift (pr_with_bindings pr_constr_expr pr_lconstr_expr))
- (lift (pr_with_bindings (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+ (lift_env (fun env sigma -> pr_with_bindings (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+ (lift_env (fun env sigma -> pr_with_bindings (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+ (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_with_bindings_env
;
register_print0 Tacarg.wit_destruction_arg
- (lift (pr_destruction_arg pr_constr_expr pr_lconstr_expr))
- (lift (pr_destruction_arg (pr_and_constr_expr pr_glob_constr_pptac) (pr_and_constr_expr pr_lglob_constr_pptac)))
+ (lift_env (fun env sigma -> pr_destruction_arg (pr_constr_expr env sigma) (pr_lconstr_expr env sigma)))
+ (lift_env (fun env sigma -> pr_destruction_arg (pr_and_constr_expr @@ pr_glob_constr_pptac env sigma)
+ (pr_and_constr_expr @@ pr_lglob_constr_pptac env sigma)))
pr_destruction_arg_env
;
register_basic_print0 Stdarg.wit_int int int int;
@@ -1379,12 +1393,12 @@ let () =
register_basic_print0 Stdarg.wit_string qstring qstring qstring
let () =
- let printer _ _ prtac = prtac in
+ let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_tactic printer printer printer
ltop (0,E)
let () =
- let pr_unit _ _ _ _ () = str "()" in
- let printer _ _ prtac = prtac in
+ let pr_unit _env _sigma _ _ _ _ () = str "()" in
+ let printer env sigma _ _ prtac = prtac env sigma in
declare_extra_genarg_pprule_with_level wit_ltac printer printer pr_unit
ltop (0,E)
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index bc47036d92..70af09833d 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -26,40 +26,46 @@ type 'a grammar_tactic_prod_item_expr =
| TacNonTerm of ('a * Names.Id.t option) Loc.located
type 'a raw_extra_genarg_printer =
- (constr_expr -> Pp.t) ->
- (constr_expr -> Pp.t) ->
- (tolerability -> raw_tactic_expr -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a glob_extra_genarg_printer =
- (glob_constr_and_expr -> Pp.t) ->
- (glob_constr_and_expr -> Pp.t) ->
- (tolerability -> glob_tactic_expr -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ 'a -> Pp.t
type 'a extra_genarg_printer =
- (EConstr.t -> Pp.t) ->
- (EConstr.t -> Pp.t) ->
- (tolerability -> Val.t -> Pp.t) ->
- 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ 'a -> Pp.t
type 'a raw_extra_genarg_printer_with_level =
- (constr_expr -> Pp.t) ->
- (constr_expr -> Pp.t) ->
- (tolerability -> raw_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> constr_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
type 'a glob_extra_genarg_printer_with_level =
- (glob_constr_and_expr -> Pp.t) ->
- (glob_constr_and_expr -> Pp.t) ->
- (tolerability -> glob_tactic_expr -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> glob_tactic_expr -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
type 'a extra_genarg_printer_with_level =
- (EConstr.constr -> Pp.t) ->
- (EConstr.constr -> Pp.t) ->
- (tolerability -> Val.t -> Pp.t) ->
- tolerability -> 'a -> Pp.t
+ Environ.env -> Evd.evar_map ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t) ->
+ (Environ.env -> Evd.evar_map -> tolerability -> Val.t -> Pp.t) ->
+ tolerability -> 'a -> Pp.t
val declare_extra_genarg_pprule :
('a, 'b, 'c) genarg_type ->
@@ -91,12 +97,13 @@ val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
val pr_with_occurrences :
('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t
-val pr_red_expr :
- ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) ->
+val pr_red_expr : env -> Evd.evar_map ->
+ (env -> Evd.evar_map -> 'a -> Pp.t) * (env -> Evd.evar_map -> 'a -> Pp.t) * ('b -> Pp.t) * (env -> Evd.evar_map -> 'c -> Pp.t) ->
('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t
val pr_may_eval :
- ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) ->
- ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
+ env -> Evd.evar_map ->
+ (env -> Evd.evar_map -> 'a -> Pp.t) -> (env -> Evd.evar_map -> 'a -> Pp.t) -> ('b -> Pp.t) ->
+ (env -> Evd.evar_map -> 'c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t
val pr_and_short_name : ('a -> Pp.t) -> 'a Genredexpr.and_short_name -> Pp.t
@@ -111,14 +118,14 @@ val pr_clauses : (* default: *) bool option ->
('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t
(* Some true = default is concl; Some false = default is all; None = no default *)
-val pr_raw_generic : env -> rlevel generic_argument -> Pp.t
+val pr_raw_generic : env -> Evd.evar_map -> rlevel generic_argument -> Pp.t
-val pr_glb_generic : env -> glevel generic_argument -> Pp.t
+val pr_glb_generic : env -> Evd.evar_map -> glevel generic_argument -> Pp.t
-val pr_raw_extend: env -> int ->
+val pr_raw_extend: env -> Evd.evar_map -> int ->
ml_tactic_entry -> raw_tactic_arg list -> Pp.t
-val pr_glob_extend: env -> int ->
+val pr_glob_extend: env -> Evd.evar_map -> int ->
ml_tactic_entry -> glob_tactic_arg list -> Pp.t
val pr_extend :
@@ -131,9 +138,9 @@ val pr_alias : (Val.t -> Pp.t) ->
val pr_ltac_constant : ltac_constant -> Pp.t
-val pr_raw_tactic : raw_tactic_expr -> Pp.t
+val pr_raw_tactic : env -> Evd.evar_map -> raw_tactic_expr -> Pp.t
-val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t
+val pr_raw_tactic_level : env -> Evd.evar_map -> tolerability -> raw_tactic_expr -> Pp.t
val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b1d5c0252f..75565c1a34 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -618,7 +618,9 @@ let solve_remaining_by env sigma holes by =
in
(* Only solve independent holes *)
let indep = List.map_filter map holes in
- let ist = { Geninterp.lfun = Id.Map.empty; extra = Geninterp.TacStore.empty } in
+ let ist = { Geninterp.lfun = Id.Map.empty
+ ; poly = false
+ ; extra = Geninterp.TacStore.empty } in
let solve_tac = match tac with
| Genarg.GenArg (Genarg.Glbwit tag, tac) ->
Ftactic.run (Geninterp.interp tag ist tac) (fun _ -> Proofview.tclUNIT ())
@@ -1790,15 +1792,15 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
-let anew_instance atts binders instance fields =
+let anew_instance ~pstate atts binders instance fields =
let program_mode = atts.program in
- new_instance ~program_mode atts.polymorphic
+ new_instance ~pstate ~program_mode atts.polymorphic
binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global:atts.global ~generalize:false ~refine:false Hints.empty_hint_info
-let declare_instance_refl atts binders a aeq n lemma =
+let declare_instance_refl ~pstate atts binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
- in anew_instance atts binders instance
+ in anew_instance ~pstate atts binders instance
[(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
let declare_instance_sym atts binders a aeq n lemma =
@@ -1811,47 +1813,44 @@ let declare_instance_trans atts binders a aeq n lemma =
in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "transitivity"),lemma)]
-let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
- let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
- in ignore(anew_instance atts binders instance []);
+ let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
+ let _, pstate = anew_instance ~pstate atts binders instance [] in
match (refl,symm,trans) with
- (None, None, None) -> ()
+ (None, None, None) -> pstate
| (Some lemma1, None, None) ->
- ignore (declare_instance_refl atts binders a aeq n lemma1)
+ snd @@ declare_instance_refl ~pstate atts binders a aeq n lemma1
| (None, Some lemma2, None) ->
- ignore (declare_instance_sym atts binders a aeq n lemma2)
+ snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
| (None, None, Some lemma3) ->
- ignore (declare_instance_trans atts binders a aeq n lemma3)
+ snd @@ declare_instance_trans ~pstate atts binders a aeq n lemma3
| (Some lemma1, Some lemma2, None) ->
- ignore (declare_instance_refl atts binders a aeq n lemma1);
- ignore (declare_instance_sym atts binders a aeq n lemma2)
+ let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+ snd @@ declare_instance_sym ~pstate atts binders a aeq n lemma2
| (Some lemma1, None, Some lemma3) ->
- let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
- let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
- let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder"
- in ignore(
- anew_instance atts binders instance
+ let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+ let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
+ snd @@ anew_instance ~pstate atts binders instance
[(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
- (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)])
+ (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
| (None, Some lemma2, Some lemma3) ->
- let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
- let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
- let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER"
- in ignore(
- anew_instance atts binders instance
+ let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+ let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
+ snd @@ anew_instance ~pstate atts binders instance
[(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
- (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)])
+ (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
| (Some lemma1, Some lemma2, Some lemma3) ->
- let _lemma_refl = declare_instance_refl atts binders a aeq n lemma1 in
- let _lemma_sym = declare_instance_sym atts binders a aeq n lemma2 in
- let _lemma_trans = declare_instance_trans atts binders a aeq n lemma3 in
- let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
- in ignore(
- anew_instance atts binders instance
+ let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
+ let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
+ let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
+ snd @@ anew_instance ~pstate atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
- (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)])
+ (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
@@ -1947,18 +1946,18 @@ let warn_add_setoid_deprecated =
CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
-let add_setoid atts binders a aeq t n =
+let add_setoid ~pstate atts binders a aeq t n =
warn_add_setoid_deprecated ?loc:a.CAst.loc ();
init_setoid ();
- let _lemma_refl = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
- let _lemma_sym = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
- let _lemma_trans = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+ let _lemma_refl, pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+ let _lemma_sym, pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+ let _lemma_trans, pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
- in ignore(
- anew_instance atts binders instance
+ in
+ snd @@ anew_instance ~pstate atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
- (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])])
+ (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
let make_tactic name =
@@ -1970,7 +1969,7 @@ let warn_add_morphism_deprecated =
CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
-let add_morphism_infer atts m n =
+let add_morphism_infer ~pstate atts m n : Proof_global.t option =
warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
(* NB: atts.program is ignored, program mode automatically set by vernacentries *)
@@ -1981,45 +1980,47 @@ let add_morphism_infer atts m n =
if Lib.is_modtype () then
let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
- (Entries.ParameterEntry
- (None,(instance,uctx),None),
- Decl_kinds.IsAssumption Decl_kinds.Logical)
+ (Entries.ParameterEntry
+ (None,(instance,uctx),None),
+ Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
- declare_projection n instance_id (ConstRef cst)
+ add_instance (Typeclasses.new_instance
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+ declare_projection n instance_id (ConstRef cst);
+ pstate
else
let kind = Decl_kinds.Global, atts.polymorphic,
- Decl_kinds.DefinitionBody Decl_kinds.Instance
+ Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
- | Globnames.ConstRef cst ->
- add_instance (Typeclasses.new_instance
- (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+ | Globnames.ConstRef cst ->
+ add_instance (Typeclasses.new_instance
+ (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
atts.global (ConstRef cst));
- declare_projection n instance_id (ConstRef cst)
- | _ -> assert false
+ declare_projection n instance_id (ConstRef cst)
+ | _ -> assert false
in
let hook = Lemmas.mk_hook hook in
- Flags.silently
- (fun () ->
- Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance);
- ignore (Pfedit.by (Tacinterp.interp tac))) ()
+ Flags.silently
+ (fun () ->
+ let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
-let add_morphism atts binders m s n =
+let add_morphism ~pstate atts binders m s n =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let instance =
(((CAst.make @@ Name instance_id),None), Explicit,
CAst.make @@ CAppExpl (
(None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None),
- [cHole; s; m]))
+ [cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
- None
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+ let _, pstate = new_instance ~pstate ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
+ None
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info in
+ pstate
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 2457b265f0..a200cb5ced 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,18 @@ val cl_rewrite_clause :
val is_applied_rewrite_relation :
env -> evar_map -> rel_context -> constr -> types option
-val declare_relation : rewrite_attributes ->
+val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
- constr_expr option -> constr_expr option -> constr_expr option -> unit
+ constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
-val add_setoid :
+val add_setoid : pstate:Proof_global.t option ->
rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
- Id.t -> unit
+ Id.t -> Proof_global.t option
-val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> unit
+val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
-val add_morphism :
- rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
+val add_morphism : pstate:Proof_global.t option ->
+ rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index eac84f0543..4398fb14ab 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -138,9 +138,10 @@ let f_debug : debug_info TacStore.field = TacStore.field ()
let f_trace : ltac_trace TacStore.field = TacStore.field ()
(* Signature for interpretation: val_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
- lfun : value Id.Map.t;
- extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+ { lfun : value Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
let extract_trace ist =
if is_traced () then match TacStore.get ist.extra f_trace with
@@ -544,12 +545,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let (_, dummy_proofview) = Proofview.init sigma [] in
(* Again this is called at times with no open proof! *)
- let name, poly =
- try
- let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
- name, poly
- with | Proof_global.NoCurrentProof -> Id.of_string "tacinterp", false
- in
+ let name, poly = Id.of_string "tacinterp", ist.poly in
let (trace,_,_,_) = Proofview.apply ~name ~poly env (push_trace (loc_of_glob_constr term,LtacConstrInterp (term,vars)) ist) dummy_proofview in
let (evd,c) =
catch_error trace (understand_ltac flags env sigma vars kind) term
@@ -566,11 +562,13 @@ let constr_flags () = {
fail_evar = true;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
(* Interprets a constr; expects evars to be solved *)
let interp_constr_gen kind ist env sigma c =
- interp_gen kind ist false (constr_flags ()) env sigma c
+ let flags = { (constr_flags ()) with polymorphic = ist.Geninterp.poly } in
+ interp_gen kind ist false flags env sigma c
let interp_constr = interp_constr_gen WithoutTypeConstraint
@@ -582,6 +580,7 @@ let open_constr_use_classes_flags () = {
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let open_constr_no_classes_flags () = {
@@ -590,6 +589,7 @@ let open_constr_no_classes_flags () = {
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let pure_open_constr_flags = {
@@ -598,6 +598,7 @@ let pure_open_constr_flags = {
fail_evar = false;
expand_evars = false;
program_mode = false;
+ polymorphic = false;
}
(* Interprets an open constr *)
@@ -1021,6 +1022,7 @@ let type_uconstr ?(flags = (constr_flags ()))
ltac_idents = closure.idents;
ltac_genargs = Id.Map.empty;
} in
+ let flags = { flags with polymorphic = ist.Geninterp.poly } in
understand_ltac flags env sigma vars expected_type term
end
@@ -1146,6 +1148,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
let alias = Tacenv.interp_alias s in
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let (>>=) = Ftactic.bind in
let interp_vars = Ftactic.List.map (fun v -> interp_tacarg ist v) l in
let tac l =
@@ -1153,8 +1156,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let lfun = List.fold_right2 addvar alias.Tacenv.alias_args l ist.lfun in
Ftactic.lift (push_trace (loc,LtacNotationCall s) ist) >>= fun trace ->
let ist = {
- lfun = lfun;
- extra = TacStore.set ist.extra f_trace trace; } in
+ lfun
+ ; poly
+ ; extra = TacStore.set ist.extra f_trace trace } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
Ftactic.lift (tactic_of_value ist v)
in
@@ -1207,12 +1211,13 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
if mustbetac then Ftactic.return (coerce_to_tactic loc id v) else Ftactic.return v
end
| ArgArg (loc,r) ->
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let ids = extract_ids [] ist.lfun Id.Set.empty in
let loc_info = (Option.default loc loc',LtacNameCall r) in
let extra = TacStore.set ist.extra f_avoid_ids ids in
push_trace loc_info ist >>= fun trace ->
let extra = TacStore.set extra f_trace trace in
- let ist = { lfun = Id.Map.empty; extra = extra; } in
+ let ist = { lfun = Id.Map.empty; poly; extra } in
let appl = GlbAppl[r,[]] in
Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false
(val_interp ~appl ist (Tacenv.interp_ltac r))
@@ -1260,6 +1265,7 @@ and interp_tacarg ist arg : Val.t Ftactic.t =
(* Interprets an application node *)
and interp_app loc ist fv largs : Val.t Ftactic.t =
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let (>>=) = Ftactic.bind in
let fail = Tacticals.New.tclZEROMSG (str "Illegal tactic application.") in
if has_type fv (topwit wit_tacvalue) then
@@ -1277,9 +1283,11 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
if List.is_empty lvar then
begin wrap_error
begin
- let ist = {
- lfun = newlfun;
- extra = TacStore.set ist.extra f_trace []; } in
+ let ist =
+ { lfun = newlfun
+ ; poly
+ ; extra = TacStore.set ist.extra f_trace []
+ } in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
(catch_error_tac trace (val_interp ist body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
@@ -1317,8 +1325,10 @@ and tactic_of_value ist vle =
if has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
| VFun (appl,trace,lfun,[],t) ->
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let ist = {
lfun = lfun;
+ poly;
extra = TacStore.set ist.extra f_trace []; } in
let tac = name_if_glob appl (eval_tactic ist t) in
Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac trace tac)
@@ -1388,6 +1398,7 @@ and interp_letin ist llc u =
(** [interp_match_success lz ist succ] interprets a single matching success
(of type {!Tactic_matching.t}). *)
and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
let (>>=) = Ftactic.bind in
let lctxt = Id.Map.map interp_context context in
let hyp_subst = Id.Map.map Value.of_constr terms in
@@ -1396,9 +1407,11 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
val_interp ist lhs >>= fun v ->
if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
| VFun (appl,trace,lfun,[],t) ->
- let ist = {
- lfun = lfun;
- extra = TacStore.set ist.extra f_trace trace; } in
+ let ist =
+ { lfun = lfun
+ ; poly
+ ; extra = TacStore.set ist.extra f_trace trace
+ } in
let tac = eval_tactic ist t in
let dummy = VFun (appl,extract_trace ist, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
@@ -1872,7 +1885,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
let default_ist () =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
- { lfun = Id.Map.empty; extra = extra }
+ { lfun = Id.Map.empty; poly = false; extra = extra }
let eval_tactic t =
Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
@@ -1912,11 +1925,12 @@ end
let interp_tac_gen lfun avoid_ids debug t =
+ Proofview.tclProofInfo [@ocaml.warning "-3"] >>= fun (_name, poly) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
- let ist = { lfun = lfun; extra = extra } in
+ let ist = { lfun; poly; extra } in
let ltacvars = Id.Map.domain lfun in
interp_tactic ist
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
@@ -2057,20 +2071,15 @@ let interp_redexp env sigma r =
(* Backwarding recursive needs of tactic glob/interp/eval functions *)
let _ =
- let eval lfun env sigma ty tac =
+ let eval lfun poly env sigma ty tac =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
- let ist = { lfun = lfun; extra; } in
+ let ist = { lfun; poly; extra; } in
let tac = interp_tactic ist tac in
- (* XXX: This depends on the global state which is bad; the hooking
- mechanism should be modified. *)
- let name, poly =
- try
- let (_, poly, _) = Proof_global.get_current_persistence () in
- let name = Proof_global.get_current_proof_name () in
- name, poly
- with | Proof_global.NoCurrentProof ->
- Id.of_string "ltac_gen", false
- in
+ (* EJGA: We sould also pass the proof name if desired, for now
+ poly seems like enough to get reasonable behavior in practice
+ *)
+ let name, poly = Id.of_string "ltac_gen", poly in
+ let name, poly = Id.of_string "ltac_gen", poly in
let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index d9c80bb835..22a092fa8b 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -39,9 +39,10 @@ module TacStore : Store.S with
and type 'a field = 'a Geninterp.TacStore.field
(** Signature for interpretation: val\_interp and interpretation functions *)
-type interp_sign = Geninterp.interp_sign = {
- lfun : value Id.Map.t;
- extra : TacStore.t }
+type interp_sign = Geninterp.interp_sign =
+ { lfun : value Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
open Genintern
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 99b9e881f6..04f3116664 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -19,11 +19,9 @@ let prtac x =
Pptactic.pr_glob_tactic (Global.env()) x
let prmatchpatt env sigma hyp =
Pptactic.pr_match_pattern (Printer.pr_constr_pattern_env env sigma) hyp
-let prmatchrl rl =
+let prmatchrl env sigma rl =
Pptactic.pr_match_rule false (Pptactic.pr_glob_tactic (Global.env()))
- (fun (_,p) ->
- let sigma, env = Pfedit.get_current_context () in
- Printer.pr_constr_pattern_env env sigma p) rl
+ (fun (_,p) -> Printer.pr_constr_pattern_env env sigma p) rl
(* This module intends to be a beginning of debugger for tactic expressions.
Currently, it is quite simple and we can hope to have, in the future, a more
@@ -246,13 +244,13 @@ let db_constr debug env sigma c =
else return ()
(* Prints the pattern rule *)
-let db_pattern_rule debug num r =
+let db_pattern_rule debug env sigma num r =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
begin
msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
- str "|" ++ spc () ++ prmatchrl r)
+ str "|" ++ spc () ++ prmatchrl env sigma r)
end
else return ()
@@ -372,7 +370,10 @@ let explain_ltac_call_trace last trace loc =
strbrk " (with " ++
prlist_with_sep pr_comma
(fun (id,c) ->
- let sigma, env = Pfedit.get_current_context () in
+ (* XXX: This hooks into the ExplainErr extension API
+ so it is tricky to provide the right env for now. *)
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders_env env sigma c)
(List.rev (Id.Map.bindings vars)) ++ str ")"
else mt())
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index 91e8510b92..74ea4e6b74 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -40,7 +40,7 @@ val db_constr : debug_info -> env -> evar_map -> constr -> unit Proofview.NonLog
(** Prints the pattern rule *)
val db_pattern_rule :
- debug_info -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
+ debug_info -> env -> evar_map -> int -> (Genintern.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> unit Proofview.NonLogical.t
(** Prints a matched hypothesis *)
val db_matched_hyp :
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:46:18 +0000