aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.mlg2
-rw-r--r--plugins/ltac/extraargs.mlg2
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_class.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg64
-rw-r--r--plugins/ltac/g_obligations.mlg14
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/leminv.ml20
-rw-r--r--plugins/ltac/pltac.ml36
-rw-r--r--plugins/ltac/pptactic.ml15
-rw-r--r--plugins/ltac/profile_ltac.ml4
-rw-r--r--plugins/ltac/profile_ltac_tactics.mlg4
-rw-r--r--plugins/ltac/rewrite.ml8
-rw-r--r--plugins/ltac/taccoerce.ml2
-rw-r--r--plugins/ltac/taccoerce.mli2
-rw-r--r--plugins/ltac/tacentries.ml10
-rw-r--r--plugins/ltac/tacexpr.ml2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml6
-rw-r--r--plugins/ltac/tacinterp.ml145
-rw-r--r--plugins/ltac/tacinterp.mli6
-rw-r--r--plugins/ltac/tacsubst.ml2
22 files changed, 186 insertions, 172 deletions
diff --git a/plugins/ltac/coretactics.mlg b/plugins/ltac/coretactics.mlg
index cb226de586..f1f538ab39 100644
--- a/plugins/ltac/coretactics.mlg
+++ b/plugins/ltac/coretactics.mlg
@@ -263,7 +263,7 @@ END
(** Double induction *)
-TACTIC EXTEND double_induction
+TACTIC EXTEND double_induction DEPRECATED { Deprecation.make () }
| [ "double" "induction" quantified_hypothesis(h1) quantified_hypothesis(h2) ] ->
{ Elim.h_double_induction h1 h2 }
END
diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index eb53fd45d0..863c4d37d8 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -25,7 +25,7 @@ open Locus
(** Adding scopes for generic arguments not defined through ARGUMENT EXTEND *)
let create_generic_quotation name e wit =
- let inject (loc, v) = Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v) in
+ let inject (loc, v) = Tacexpr.TacGeneric (Some name, Genarg.in_gen (Genarg.rawwit wit) v) in
Tacentries.create_ltac_quotation name inject (e, None)
let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 66c72a30a2..4f20e5a800 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -43,7 +43,7 @@ DECLARE PLUGIN "ltac_plugin"
(**********************************************************************)
(* replace, discriminate, injection, simplify_eq *)
-(* cutrewrite, dependent rewrite *)
+(* dependent rewrite *)
let with_delayed_uconstr ist c tac =
let flags = {
@@ -203,12 +203,6 @@ TACTIC EXTEND dependent_rewrite
-> { rewriteInHyp b c id }
END
-TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn }
-| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
- -> { cutRewriteInHyp b eqn id }
-END
-
(**********************************************************************)
(* Decompose *)
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 35c90444b1..8d197e6056 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -77,7 +77,7 @@ END
(* true = All transparent, false = Opaque if possible *)
VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF
- | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> {
+ | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) integer_opt(depth) ] -> {
set_typeclasses_debug d;
Option.iter set_typeclasses_strategy s;
set_typeclasses_depth depth
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 114acaa412..6cf5d30a95 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -48,14 +48,14 @@ let reference_to_id qid =
CErrors.user_err ?loc:qid.CAst.loc
(str "This expression should be a simple identifier.")
-let tactic_mode = Entry.create "vernac:tactic_command"
+let tactic_mode = Entry.create "tactic_command"
let new_entry name =
let e = Entry.create name in
e
-let toplevel_selector = new_entry "vernac:toplevel_selector"
-let tacdef_body = new_entry "tactic:tacdef_body"
+let toplevel_selector = new_entry "toplevel_selector"
+let tacdef_body = new_entry "tacdef_body"
(* Registers [tactic_mode] as a parser for proof editing *)
let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
@@ -180,7 +180,7 @@ GRAMMAR EXTEND Gram
[ [ a = tactic_arg -> { a }
| c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) }
(* Unambiguous entries: tolerated w/o "ltac:" modifier *)
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
(* Can be used as argument and at toplevel in tactic expressions. *)
tactic_arg:
@@ -209,9 +209,9 @@ GRAMMAR EXTEND Gram
| c = Constr.constr -> { ConstrTerm c } ] ]
;
tactic_atom:
- [ [ n = integer -> { TacGeneric (genarg_of_int n) }
+ [ [ n = integer -> { TacGeneric (None, genarg_of_int n) }
| r = reference -> { TacCall (CAst.make ~loc (r,[])) }
- | "()" -> { TacGeneric (genarg_of_unit ()) } ] ]
+ | "()" -> { TacGeneric (None, genarg_of_unit ()) } ] ]
;
match_key:
[ [ "match" -> { Once }
@@ -271,7 +271,7 @@ GRAMMAR EXTEND Gram
message_token:
[ [ id = identref -> { MsgIdent id }
| s = STRING -> { MsgString s }
- | n = integer -> { MsgInt n } ] ]
+ | n = natural -> { MsgInt n } ] ]
;
ltac_def_kind:
@@ -355,28 +355,8 @@ GRAMMAR EXTEND Gram
open Stdarg
open Tacarg
open Vernacextend
-open Goptions
open Libnames
-let print_info_trace =
- declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
-
-let vernac_solve ~pstate n info tcom b =
- let open Goal_select in
- let pstate, status = Declare.Proof.map_fold_endline ~f:(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) =
- Proof.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;
- pstate
-
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
}
@@ -409,34 +389,34 @@ END
{
-let is_anonymous_abstract = function
- | TacAbstract (_,None) -> true
- | TacSolve [TacAbstract (_,None)] -> true
- | _ -> false
let rm_abstract = function
- | TacAbstract (t,_) -> t
- | TacSolve [TacAbstract (t,_)] -> TacSolve [t]
- | x -> x
+ | TacAbstract (t,_) -> t, true
+ | TacSolve [TacAbstract (t,_)] -> TacSolve [t], true
+ | x -> x, false
let is_explicit_terminator = function TacSolve _ -> true | _ -> false
}
VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
-| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ ltac_selector_opt(g) ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- vernac_solve g n t def
+ let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in
+ ComTactic.solve g ~info t ~with_end_tac
}
-| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+END
+
+VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof
+| [ "par" ":" ltac_info_opt(info) tactic(t) ltac_use_default(with_end_tac) ] =>
{
- let anon_abstracting_tac = is_anonymous_abstract t in
let solving_tac = is_explicit_terminator t in
- let parallel = `Yes (solving_tac,anon_abstracting_tac) in
let pbr = if solving_tac then Some "par" else None in
- VtProofStep{ parallel = parallel; proof_block_detection = pbr }
+ VtProofStep{ proof_block_detection = pbr }
} -> {
- let t = rm_abstract t in
- vernac_solve Goal_select.SelectAll n t def
+ let t, abstract = rm_abstract t in
+ let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in
+ ComTactic.solve_parallel ~info t ~abstract ~with_end_tac
}
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index fa176482bf..fc24475a62 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -56,7 +56,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
Genarg.create_arg "withtac"
-let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac)
}
@@ -88,13 +88,13 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_program
-| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" natural(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" natural(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" natural(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
@@ -102,9 +102,9 @@ VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE declare_
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF STATE program
-| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "of" ident(name) "with" tactic(t) ] ->
{ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) }
-| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] ->
+| [ "Solve" "Obligation" natural(num) "with" tactic(t) ] ->
{ try_solve_obligation num None (Some (Tacinterp.interp t)) }
END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 09cdc997ab..8331927cda 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -219,7 +219,7 @@ type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
-let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
let () =
let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml
index 0024d1a4ba..f42c1f73a3 100644
--- a/plugins/ltac/leminv.ml
+++ b/plugins/ltac/leminv.ml
@@ -228,14 +228,15 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let p = EConstr.to_constr sigma invProof in
- p, sigma
+ invProof, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
- let univs = Evd.univ_entry ~poly sigma in
- let entry = Declare.definition_entry ~univs invProof in
- let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Lemma) (Declare.DefinitionEntry entry) in
+ let cinfo = Declare.CInfo.make ~name ~typ:None () in
+ let info = Declare.Info.make ~poly ~kind:Decls.(IsProof Lemma) () in
+ let _ : Names.GlobRef.t =
+ Declare.declare_definition ~cinfo ~info ~opaque:false ~body:invProof sigma
+ in
()
(* inv_op = Inv (derives de complete inv. lemma)
@@ -244,13 +245,10 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let add_inversion_lemma_exn ~poly na com comsort bool tac =
let env = Global.env () in
let sigma = Evd.from_env env in
- let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in
+ let c, uctx = Constrintern.interp_type env sigma com in
+ let sigma = Evd.from_ctx uctx in
let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in
- try
- add_inversion_lemma ~poly na env sigma c sort bool tac
- with
- | UserError (Some "Case analysis",s) -> (* Reference to Indrec *)
- user_err ~hdr:"Inv needs Nodep Prop Set" s
+ add_inversion_lemma ~poly na env sigma c sort bool tac
(* ================================= *)
(* Applying a given inversion lemma *)
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 5b5ee64a56..b7b54143df 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,39 +11,37 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Entry.create "tactic:simple_tactic"
-
-let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
+let simple_tactic = Entry.create "simple_tactic"
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic "open_constr"
+ Entry.create "open_constr"
let constr_with_bindings =
- make_gen_entry utactic "constr_with_bindings"
+ Entry.create "constr_with_bindings"
let bindings =
- make_gen_entry utactic "bindings"
+ Entry.create "bindings"
let hypident = Entry.create "hypident"
-let constr_may_eval = make_gen_entry utactic "constr_may_eval"
-let constr_eval = make_gen_entry utactic "constr_eval"
+let constr_may_eval = Entry.create "constr_may_eval"
+let constr_eval = Entry.create "constr_eval"
let uconstr =
- make_gen_entry utactic "uconstr"
+ Entry.create "uconstr"
let quantified_hypothesis =
- make_gen_entry utactic "quantified_hypothesis"
-let destruction_arg = make_gen_entry utactic "destruction_arg"
-let int_or_var = make_gen_entry utactic "int_or_var"
+ Entry.create "quantified_hypothesis"
+let destruction_arg = Entry.create "destruction_arg"
+let int_or_var = Entry.create "int_or_var"
let simple_intropattern =
- make_gen_entry utactic "simple_intropattern"
-let in_clause = make_gen_entry utactic "in_clause"
+ Entry.create "simple_intropattern"
+let in_clause = Entry.create "in_clause"
let clause_dft_concl =
- make_gen_entry utactic "clause"
+ Entry.create "clause"
(* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic:tactic_arg"
-let tactic_expr = make_gen_entry utactic "tactic_expr"
-let binder_tactic = make_gen_entry utactic "binder_tactic"
+let tactic_arg = Entry.create "tactic_arg"
+let tactic_expr = Entry.create "tactic_expr"
+let binder_tactic = Entry.create "binder_tactic"
-let tactic = make_gen_entry utactic "tactic"
+let tactic = Entry.create "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6233807016..cbb53497d3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -179,7 +179,7 @@ let string_of_genarg_arg (ArgumentType arg) =
| ConstrTypeOf c ->
hov 1 (keyword "type of" ++ spc() ++ prc env sigma c)
| ConstrTerm c when test c ->
- h 0 (str "(" ++ prc env sigma c ++ str ")")
+ h (str "(" ++ prc env sigma c ++ str ")")
| ConstrTerm c ->
prc env sigma c
@@ -338,8 +338,8 @@ let string_of_genarg_arg (ArgumentType arg) =
| Extend.Uentryl (_, l) -> prtac LevelSome arg
| _ ->
match arg with
- | TacGeneric arg ->
- let pr l arg = prtac l (TacGeneric arg) in
+ | TacGeneric (isquot,arg) ->
+ let pr l arg = prtac l (TacGeneric (isquot,arg)) in
pr_any_arg pr symb arg
| _ -> str "ltac:(" ++ prtac LevelSome arg ++ str ")"
@@ -571,7 +571,7 @@ let pr_goal_selector ~toplevel s =
let pr_let_clause k pr_gen pr_arg (na,(bl,t)) =
let pr = function
- | TacGeneric arg ->
+ | TacGeneric (_,arg) ->
let name = string_of_genarg_arg (genarg_tag arg) in
if name = "unit" || name = "int" then
(* Hard-wired parsing rules *)
@@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s =
++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
)
| TacChange (check,op,c,h) ->
- let name = if check then "change_no_check" else "change" in
+ let name = if check then "change" else "change_no_check" in
hov 1 (
primitive name ++ brk (1,1)
++ (
@@ -1049,8 +1049,9 @@ let pr_goal_selector ~toplevel s =
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 env sigma arg, latom
+ | TacArg { CAst.v=TacGeneric (isquot,arg) } ->
+ let p = pr.pr_generic env sigma arg in
+ (match isquot with Some name -> str name ++ str ":(" ++ p ++ str ")" | None -> p), latom
| TacArg { CAst.v=TacCall {CAst.v=(f,[])} } ->
pr.pr_reference f, latom
| TacArg { CAst.v=TacCall {CAst.loc; v=(f,l)} } ->
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0dbf16a821..9c15d24dd3 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -146,7 +146,7 @@ let header =
fnl ()
let rec print_node ~filter all_total indent prefix (s, e) =
- h 0 (
+ h (
padr_with '-' 40 (prefix ^ s ^ " ")
++ padl 7 (format_ratio (e.local /. all_total))
++ padl 7 (format_ratio (e.total /. all_total))
@@ -212,7 +212,7 @@ let to_string ~filter ?(cutoff=0.0) node =
in
let filter s n = filter s && (all_total <= 0.0 || n /. all_total >= cutoff /. 100.0) in
let msg =
- h 0 (str "total time: " ++ padl 11 (format_sec (all_total))) ++
+ h (str "total time: " ++ padl 11 (format_sec (all_total))) ++
fnl () ++
fnl () ++
header ++
diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg
index eb9d9cbdce..e5309ea441 100644
--- a/plugins/ltac/profile_ltac_tactics.mlg
+++ b/plugins/ltac/profile_ltac_tactics.mlg
@@ -55,7 +55,7 @@ END
TACTIC EXTEND show_ltac_profile
| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
+| [ "show" "ltac" "profile" "cutoff" integer(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) }
| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s }
END
@@ -74,7 +74,7 @@ END
VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY
| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff }
-| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) }
+| [ "Show" "Ltac" "Profile" "CutOff" integer(n) ] -> { print_results ~cutoff:(float_of_int n) }
END
VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index fb149071c9..5ef76dbdc1 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -181,7 +181,7 @@ end) = struct
fun env sigma -> class_info env sigma (Lazy.force r)
let proper_proj env sigma =
- mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+ mkConst (Option.get (List.hd (proper_class env sigma).cl_projs).meth_const)
let proper_type env (sigma,cstrs) =
let l = (proper_class env sigma).cl_impl in
@@ -498,7 +498,7 @@ let rec decompose_app_rel env evd t =
let decompose_app_rel env evd t =
let (rel, t1, t2) = decompose_app_rel env evd t in
- let ty = Retyping.get_type_of env evd rel in
+ let ty = try Retyping.get_type_of ~lax:true env evd rel with Retyping.RetypeError _ -> error_no_relation () in
let () = if not (Reductionops.is_arity env evd ty) then error_no_relation () in
(rel, t1, t2)
@@ -546,7 +546,7 @@ let rewrite_core_unif_flags = {
Unification.check_applied_meta_types = true;
Unification.use_pattern_unification = true;
Unification.use_meta_bound_pattern_unification = true;
- Unification.allowed_evars = Unification.AllowAll;
+ Unification.allowed_evars = Evarsolve.AllowedEvars.all;
Unification.restrict_conv_on_strict_subterms = false;
Unification.modulo_betaiota = false;
Unification.modulo_eta = true;
@@ -2144,7 +2144,7 @@ let setoid_proof ty fn fallback =
let car = snd (List.hd (fst (Reductionops.splay_prod env sigma t))) in
(try init_relation_classes () with _ -> raise Not_found);
fn env sigma car rel
- with e ->
+ with e when CErrors.noncritical e ->
(* XXX what is the right test here as to whether e can be converted ? *)
let e, info = Exninfo.capture e in
Proofview.tclZERO ~info e
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 91d26519b8..f7037176d2 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -394,7 +394,7 @@ type appl =
(* Values for interpretation *)
type tacvalue =
- | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
Name.t list * Tacexpr.glob_tactic_expr
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 3afbb56b23..b8592c5c76 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -104,7 +104,7 @@ type appl =
(** For calls to global constants, some may alias other. *)
type tacvalue =
- | VFun of appl*Tacexpr.ltac_trace * Val.t Id.Map.t *
+ | VFun of appl *Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t *
Name.t list * Tacexpr.glob_tactic_expr
| VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f8c25d5dd0..f0ca813b08 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -174,7 +174,7 @@ let add_tactic_entry (kn, ml, tg) state =
if Genarg.has_type arg wit && not ml then
Tacexp (Genarg.out_gen wit arg)
else
- TacGeneric arg
+ TacGeneric (None, arg)
in
let l = List.map map l in
(TacAlias (CAst.make ~loc (kn,l)):raw_tactic_expr)
@@ -349,7 +349,7 @@ let extend_atomic_tactic name entries =
| TacNonTerm (_, (symb, _)) ->
let EntryName (typ, e) = prod_item_of_symbol 0 symb in
let Genarg.Rawwit wit = typ in
- let inj x = TacArg (CAst.make @@ TacGeneric (Genarg.in_gen typ x)) in
+ let inj x = TacArg (CAst.make @@ TacGeneric (None, Genarg.in_gen typ x)) in
let default = epsilon_value inj e in
match default with
| None -> raise NonEmptyArgument
@@ -780,7 +780,7 @@ let ml_val_tactic_extend ~plugin ~name ~local ?deprecation sign tac =
let ml_tactic_name = { mltac_tactic = name; mltac_plugin = plugin } in
let len = ml_sig_len sign in
let vars = List.init len (fun i -> Id.of_string (Printf.sprintf "arg%i" i)) in
- let body = TacGeneric (in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
+ let body = TacGeneric (None, in_tacval { tacval_tac = ml_tactic_name; tacval_var = vars }) in
let vars = List.map (fun id -> Name id) vars in
let body = Tacexpr.TacFun (vars, Tacexpr.TacArg (CAst.make body)) in
let id = Names.Id.of_string name in
@@ -869,14 +869,14 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
let () = Pcoq.register_grammar wit e in
e
| Vernacextend.Arg_rules rules ->
- let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+ let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
let () = Pcoq.grammar_extend e {pos=None; data=[(None, None, rules)]} in
e
in
let (rpr, gpr, tpr) = arg.arg_printer in
let () = Pptactic.declare_extra_genarg_pprule wit rpr gpr tpr in
let () = create_ltac_quotation name
- (fun (loc, v) -> Tacexpr.TacGeneric (Genarg.in_gen (Genarg.rawwit wit) v))
+ (fun (loc, v) -> Tacexpr.TacGeneric (Some name,Genarg.in_gen (Genarg.rawwit wit) v))
(entry, None)
in
(wit, entry)
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index b261096b63..eaedf8d9c1 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -154,7 +154,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 650349b586..50767821e4 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -153,7 +153,7 @@ constraint 'a = <
(** Possible arguments of a tactic definition *)
type 'a gen_tactic_arg =
- | TacGeneric of 'lev generic_argument
+ | TacGeneric of string option * 'lev generic_argument
| ConstrMayEval of ('trm,'cst,'pat) may_eval
| Reference of 'ref
| TacCall of ('ref * 'a gen_tactic_arg list) CAst.t
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index afa79a88db..dea216045e 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -195,7 +195,7 @@ let intern_non_tactic_reference strict ist qid =
if qualid_is_ident qid && not strict then
let id = qualid_basename qid in
let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in
- TacGeneric ipat
+ TacGeneric (None,ipat)
else
(* Reference not found *)
let _, info = Exninfo.capture exn in
@@ -713,9 +713,9 @@ and intern_tacarg strict onlytac ist = function
| TacPretype c -> TacPretype (intern_constr ist c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (intern_tactic onlytac ist t)
- | TacGeneric arg ->
+ | TacGeneric (isquot,arg) ->
let arg = intern_genarg ist arg in
- TacGeneric arg
+ TacGeneric (isquot,arg)
(* Reads the rules of a Match Context or a Match *)
and intern_match_rule onlytac ist ?(as_type=false) = function
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fdebe14a23..eaeae50254 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -124,7 +124,7 @@ let is_traced () =
let name_vfun appl vle =
if is_traced () && has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
- | VFun (appl0,trace,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,lfun,vars,t))
+ | VFun (appl0,trace,loc,lfun,vars,t) -> of_tacvalue (VFun (combine_appl appl0 appl,trace,loc,lfun,vars,t))
| _ -> vle
else vle
@@ -134,6 +134,7 @@ let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
(* ids inherited from the call context (needed to get fresh ids) *)
let f_debug : debug_info TacStore.field = TacStore.field ()
let f_trace : ltac_trace TacStore.field = TacStore.field ()
+let f_loc : Loc.t TacStore.field = TacStore.field ()
(* Signature for interpretation: val_interp and interpretation functions *)
type interp_sign = Geninterp.interp_sign =
@@ -141,12 +142,23 @@ type interp_sign = Geninterp.interp_sign =
; poly : bool
; extra : TacStore.t }
+let add_extra_trace trace extra = TacStore.set extra f_trace trace
let extract_trace ist =
if is_traced () then match TacStore.get ist.extra f_trace with
| None -> []
| Some l -> l
else []
+let add_extra_loc loc extra =
+ match loc with
+ | None -> extra
+ | Some loc -> TacStore.set extra f_loc loc
+let add_loc loc ist =
+ match loc with
+ | None -> ist
+ | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc }
+let extract_loc ist = TacStore.get ist.extra f_loc
+
let print_top_val env v = Pptactic.pr_value Pptactic.ltop v
let catching_error call_trace fail (e, info) =
@@ -161,27 +173,45 @@ let catching_error call_trace fail (e, info) =
fail located_exc
end
-let update_loc ?loc (e, info) =
- (e, Option.cata (Loc.add_loc info) info loc)
+let update_loc loc use_finer (e, info as e') =
+ match loc with
+ | Some loc ->
+ if use_finer then
+ (* ensure loc if there is none *)
+ match Loc.get_loc info with
+ | None -> (e, Loc.add_loc info loc)
+ | _ -> (e, info)
+ else
+ (* override loc (because loc refers to inside of Ltac functions) *)
+ (e, Loc.add_loc info loc)
+ | None -> e'
-let catch_error ?loc call_trace f x =
+let catch_error_with_trace_loc loc use_finer call_trace f x =
try f x
with e when CErrors.noncritical e ->
let e = Exninfo.capture e in
- let e = update_loc ?loc e in
+ let e = update_loc loc use_finer e in
catching_error call_trace Exninfo.iraise e
-let catch_error_loc ?loc tac =
- Proofview.tclOR tac (fun exn ->
- let (e, info) = update_loc ?loc exn in
+let catch_error_loc loc use_finer tac =
+ Proofview.tclORELSE tac (fun exn ->
+ let (e, info) = update_loc loc use_finer exn in
Proofview.tclZERO ~info e)
-let wrap_error ?loc tac k =
+let wrap_error tac k =
+ if is_traced () then Proofview.tclORELSE tac k else tac
+
+let wrap_error_loc loc use_finer tac k =
if is_traced () then Proofview.tclORELSE tac k
- else catch_error_loc ?loc tac
+ else catch_error_loc loc use_finer tac
+
+let catch_error_tac call_trace tac =
+ wrap_error
+ tac
+ (catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
-let catch_error_tac ?loc call_trace tac =
- wrap_error ?loc
+let catch_error_tac_loc loc use_finer call_trace tac =
+ wrap_error_loc loc use_finer
tac
(catching_error call_trace (fun (e, info) -> Proofview.tclZERO ~info e))
@@ -204,7 +234,7 @@ let pr_inspect env expr result =
let pp_result =
if has_type result (topwit wit_tacvalue) then
match to_tacvalue result with
- | VFun (_,_, ist, ul, b) ->
+ | VFun (_, _, _, ist, ul, b) ->
let body = if List.is_empty ul then b else (TacFun (ul, b)) in
str "a closure with body " ++ fnl() ++ pr_closure env ist body
| VRec (ist, body) ->
@@ -231,10 +261,10 @@ let propagate_trace ist loc id v =
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
- | VFun (appl,_,lfun,it,b) ->
+ | VFun (appl,_,_,lfun,it,b) ->
let t = if List.is_empty it then b else TacFun (it,b) in
let trace = push_trace(loc,LtacVarCall (id,t)) ist in
- let ans = VFun (appl,trace,lfun,it,b) in
+ let ans = VFun (appl,trace,loc,lfun,it,b) in
Proofview.tclUNIT (of_tacvalue ans)
| _ -> Proofview.tclUNIT v
else Proofview.tclUNIT v
@@ -242,7 +272,7 @@ let propagate_trace ist loc id v =
let append_trace trace v =
if has_type v (topwit wit_tacvalue) then
match to_tacvalue v with
- | VFun (appl,trace',lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,lfun,it,b))
+ | VFun (appl,trace',loc,lfun,it,b) -> of_tacvalue (VFun (appl,trace'@trace,loc,lfun,it,b))
| _ -> v
else v
@@ -254,7 +284,7 @@ let coerce_to_tactic loc id v =
if has_type v (topwit wit_tacvalue) then
let tacv = to_tacvalue v in
match tacv with
- | VFun _ -> v
+ | VFun (appl,trace,_,lfun,it,b) -> of_tacvalue (VFun (appl,trace,loc,lfun,it,b))
| _ -> fail ()
else fail ()
@@ -553,7 +583,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
let loc = loc_of_glob_constr term in
let trace = push_trace (loc,LtacConstrInterp (term,vars)) ist in
let (evd,c) =
- catch_error ?loc trace (understand_ltac flags env sigma vars kind) term
+ catch_error_with_trace_loc loc true trace (understand_ltac flags env sigma vars kind) term
in
(* spiwack: to avoid unnecessary modifications of tacinterp, as this
function already use effect, I call [run] hoping it doesn't mess
@@ -1044,7 +1074,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
function. *)
let value_interp ist = match tac with
| TacFun (it, body) ->
- Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, it, body)))
+ Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, it, body)))
| TacLetIn (true,l,u) -> interp_letrec ist l u
| TacLetIn (false,l,u) -> interp_letin ist l u
| TacMatchGoal (lz,lr,lmr) -> interp_match_goal ist lz lr lmr
@@ -1052,7 +1082,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| TacArg {loc;v} -> interp_tacarg ist v
| t ->
(* Delayed evaluation *)
- Ftactic.return (of_tacvalue (VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], t)))
+ Ftactic.return (of_tacvalue (VFun (UnnamedAppl, extract_trace ist, extract_loc ist, ist.lfun, [], t)))
in
let open Ftactic in
Control.check_for_interrupt ();
@@ -1066,12 +1096,12 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti
| _ -> value_interp ist >>= fun v -> return (name_vfun appl v)
-and eval_tactic ist tac : unit Proofview.tactic = match tac with
+and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with
| TacAtom {loc;v=t} ->
let call = LtacAtomCall t in
let trace = push_trace(loc,call) ist in
Profile_ltac.do_profile "eval_tactic:2" trace
- (catch_error_tac ?loc trace (interp_atomic ist t))
+ (catch_error_tac_loc loc true trace (interp_atomic ist t))
| TacFun _ | TacLetIn _ | TacMatchGoal _ | TacMatch _ -> interp_tactic ist tac
| TacId [] -> Proofview.tclLIFT (db_breakpoint (curr_debug ist) [])
| TacId s ->
@@ -1145,7 +1175,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l)
| TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l)
| TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac)
- | TacArg a -> interp_tactic ist (TacArg a)
+ | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v)
| TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac)
(* For extensions *)
| TacAlias {loc; v=(s,l)} ->
@@ -1160,9 +1190,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let ist = {
lfun
; poly
- ; extra = TacStore.set ist.extra f_trace trace } in
+ ; extra = add_extra_loc loc (add_extra_trace trace ist.extra) } in
val_interp ist alias.Tacenv.alias_body >>= fun v ->
- Ftactic.lift (catch_error_loc ?loc (tactic_of_value ist v))
+ Ftactic.lift (tactic_of_value ist v)
in
let tac =
Ftactic.with_env interp_vars >>= fun (env, lr) ->
@@ -1191,7 +1221,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = Ftactic.List.map_right (fun a -> interp_tacarg ist a) l in
let tac args =
let name _ _ = Pptactic.pr_extend (fun v -> print_top_val () v) 0 opn args in
- Proofview.Trace.name_tactic name (catch_error_tac ?loc trace (tac args ist))
+ Proofview.Trace.name_tactic name (catch_error_tac_loc loc false trace (tac args ist))
in
Ftactic.run args tac
@@ -1225,11 +1255,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t =
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))
+ (catch_error_tac_loc (* interp *) loc false trace
+ (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r)))
and interp_tacarg ist arg : Val.t Ftactic.t =
match arg with
- | TacGeneric arg -> interp_genarg ist arg
+ | TacGeneric (_,arg) -> interp_genarg ist arg
| Reference r -> interp_ltac_reference false ist r
| ConstrMayEval c ->
Ftactic.enter begin fun gl ->
@@ -1279,8 +1310,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
is not a tactic that expects arguments.
Otherwise Ltac goes into an infinite loop (val_interp puts
a VFun back on body, and then interp_app is called again...) *)
- | (VFun(appl,trace,olfun,(_::_ as var),body)
- |VFun(appl,trace,olfun,([] as var),
+ | (VFun(appl,trace,_,olfun,(_::_ as var),body)
+ |VFun(appl,trace,_,olfun,([] as var),
(TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
let (extfun,lvar,lval)=head_with_value (var,largs) in
let fold accu (id, v) = Id.Map.add id v accu in
@@ -1294,7 +1325,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
; extra = TacStore.set ist.extra f_trace []
} in
Profile_ltac.do_profile "interp_app" trace ~count_call:false
- (catch_error_tac ?loc trace (val_interp ist body)) >>= fun v ->
+ (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v ->
Ftactic.return (name_vfun (push_appl appl largs) v)
end
begin fun (e, info) ->
@@ -1315,8 +1346,8 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
end <*>
if List.is_empty lval then Ftactic.return v else interp_app loc ist v lval
else
- Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,newlfun,lvar,body)))
- | (VFun(appl,trace,olfun,[],body)) ->
+ Ftactic.return (of_tacvalue (VFun(push_appl appl largs,trace,loc,newlfun,lvar,body)))
+ | (VFun(appl,trace,_,olfun,[],body)) ->
let extra_args = List.length largs in
let info = Exninfo.reify () in
Tacticals.New.tclZEROMSG ~info
@@ -1335,15 +1366,15 @@ and interp_app loc ist fv largs : Val.t Ftactic.t =
and tactic_of_value ist vle =
if has_type vle (topwit wit_tacvalue) then
match to_tacvalue vle with
- | VFun (appl,trace,lfun,[],t) ->
+ | VFun (appl,trace,loc,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)
- | VFun (appl,_,vmap,vars,_) ->
+ let tac = name_if_glob appl (eval_tactic_ist ist t) in
+ Profile_ltac.do_profile "tactic_of_value" trace (catch_error_tac_loc loc false trace tac)
+ | VFun (appl,_,loc,vmap,vars,_) ->
let tactic_nm =
match appl with
UnnamedAppl -> "An unnamed user-defined tactic"
@@ -1422,14 +1453,14 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } =
let ist = { ist with lfun } in
val_interp ist lhs >>= fun v ->
if has_type v (topwit wit_tacvalue) then match to_tacvalue v with
- | VFun (appl,trace,lfun,[],t) ->
+ | VFun (appl,trace,loc,lfun,[],t) ->
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
+ let tac = eval_tactic_ist ist t in
+ let dummy = VFun (appl, extract_trace ist, loc, Id.Map.empty, [], TacId []) in
catch_error_tac trace (tac <*> Ftactic.return (of_tacvalue dummy))
| _ -> Ftactic.return v
else Ftactic.return v
@@ -1909,11 +1940,11 @@ let default_ist () =
let eval_tactic t =
Proofview.tclUNIT () >>= fun () -> (* delay for [default_ist] *)
Proofview.tclLIFT db_initialize <*>
- interp_tactic (default_ist ()) t
+ eval_tactic_ist (default_ist ()) t
let eval_tactic_ist ist t =
Proofview.tclLIFT db_initialize <*>
- interp_tactic ist t
+ eval_tactic_ist ist t
(** FFI *)
@@ -1922,7 +1953,7 @@ module Value = struct
include Taccoerce.Value
let of_closure ist tac =
- let closure = VFun (UnnamedAppl,extract_trace ist, ist.lfun, [], tac) in
+ let closure = VFun (UnnamedAppl, extract_trace ist, None, ist.lfun, [], tac) in
of_tacvalue closure
let apply_expr f args =
@@ -1959,22 +1990,26 @@ let interp_tac_gen lfun avoid_ids debug t =
let extra = TacStore.set extra f_avoid_ids avoid_ids in
let ist = { lfun; poly; extra } in
let ltacvars = Id.Map.domain lfun in
- interp_tactic ist
+ eval_tactic_ist ist
(intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars } t)
end
let interp t = interp_tac_gen Id.Map.empty Id.Set.empty (get_debug()) t
+(* MUST be marshallable! *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
+
(* Used to hide interpretation for pretty-print, now just launch tactics *)
(* [global] means that [t] should be internalized outside of goals. *)
-let hide_interp global t ot =
+let hide_interp {global;ast} =
let hide_interp env =
let ist = Genintern.empty_glob_sign env in
- let te = intern_pure_tactic ist t in
+ let te = intern_pure_tactic ist ast in
let t = eval_tactic te in
- match ot with
- | None -> t
- | Some t' -> Tacticals.New.tclTHEN t t'
+ t
in
if global then
Proofview.tclENV >>= fun env ->
@@ -1984,6 +2019,8 @@ let hide_interp global t ot =
hide_interp (Proofview.Goal.env gl)
end
+let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp
+
(***************************************************************************)
(** Register standard arguments *)
@@ -2010,6 +2047,9 @@ let () =
declare_uniform wit_int
let () =
+ declare_uniform wit_nat
+
+let () =
declare_uniform wit_bool
let () =
@@ -2076,7 +2116,7 @@ let () =
register_interp0 wit_tactic interp
let () =
- let interp ist tac = interp_tactic ist tac >>= fun () -> Ftactic.return () in
+ let interp ist tac = eval_tactic_ist ist tac >>= fun () -> Ftactic.return () in
register_interp0 wit_ltac interp
let () =
@@ -2103,12 +2143,11 @@ let _ =
let eval lfun poly env sigma ty tac =
let extra = TacStore.set TacStore.empty f_debug (get_debug ()) in
let ist = { lfun; poly; extra; } in
- let tac = interp_tactic ist tac in
+ let tac = eval_tactic_ist ist tac in
(* EJGA: We should 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 name = Id.of_string "ltac_gen" in
let (c, sigma) = Proof.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 cbb17bf0fa..01d7306c9d 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -126,8 +126,12 @@ val interp_tac_gen : value Id.Map.t -> Id.Set.t ->
val interp : raw_tactic_expr -> unit Proofview.tactic
(** Hides interpretation for pretty-print *)
+type tactic_expr = {
+ global: bool;
+ ast: Tacexpr.raw_tactic_expr;
+}
-val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> unit Proofview.tactic
+val hide_interp : tactic_expr ComTactic.tactic_interpreter
(** Internals that can be useful for syntax extensions. *)
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index c2f1589b74..fd869b225f 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -237,7 +237,7 @@ and subst_tacarg subst = function
| TacPretype c -> TacPretype (subst_glob_constr subst c)
| TacNumgoals -> TacNumgoals
| Tacexp t -> Tacexp (subst_tactic subst t)
- | TacGeneric arg -> TacGeneric (subst_genarg subst arg)
+ | TacGeneric (isquot,arg) -> TacGeneric (isquot,subst_genarg subst arg)
(* Reads the rules of a Match Context or a Match *)
and subst_match_rule subst = function
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:03:27 +0000