aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/extratactics.ml48
-rw-r--r--plugins/ltac/g_auto.ml43
-rw-r--r--plugins/ltac/g_class.ml41
-rw-r--r--plugins/ltac/g_eqdecide.ml41
-rw-r--r--plugins/ltac/g_ltac.ml411
-rw-r--r--plugins/ltac/g_obligations.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/g_tactic.ml45
-rw-r--r--plugins/ltac/pptactic.ml98
-rw-r--r--plugins/ltac/pptactic.mli70
-rw-r--r--plugins/ltac/pptacticsig.mli81
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--plugins/ltac/rewrite.mli6
-rw-r--r--plugins/ltac/tacentries.ml17
-rw-r--r--plugins/ltac/tacentries.mli2
-rw-r--r--plugins/ltac/tacexpr.mli2
-rw-r--r--plugins/ltac/tacintern.ml10
-rw-r--r--plugins/ltac/tacinterp.ml49
-rw-r--r--plugins/ltac/tacinterp.mli2
-rw-r--r--plugins/ltac/tacsubst.ml4
-rw-r--r--plugins/ltac/tauto.ml2
21 files changed, 153 insertions, 225 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 1223f6eb4b..7a9fc6657e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -38,7 +38,7 @@ let with_delayed_uconstr ist c tac =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
@@ -341,10 +341,10 @@ END
(**********************************************************************)
(* Refine *)
-let constr_flags = {
+let constr_flags () = {
Pretyping.use_typeclasses = true;
Pretyping.solve_unification_constraints = true;
- Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic;
+ Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true }
@@ -353,7 +353,7 @@ let refine_tac ist simple with_classes c =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags =
- { constr_flags with Pretyping.use_typeclasses = with_classes } in
+ { constr_flags () with Pretyping.use_typeclasses = with_classes } in
let expected_type = Pretyping.OfType concl in
let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
let update = { run = fun sigma -> c.delayed env sigma } in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 4ec42c676f..f75ea70872 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -16,6 +16,7 @@ open Pcoq.Constr
open Pltac
open Hints
open Tacexpr
+open Names
DECLARE PLUGIN "g_auto"
@@ -44,7 +45,7 @@ let eval_uconstrs ist cs =
let flags = {
Pretyping.use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some Pfedit.solve_by_implicit_tactic;
+ use_hook = Pfedit.solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true
} in
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index a28132a4b0..ca9537c824 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -13,6 +13,7 @@ open Class_tactics
open Pltac
open Stdarg
open Tacarg
+open Names
DECLARE PLUGIN "g_class"
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 905653281c..679aa11272 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -15,6 +15,7 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Eqdecide
+open Names
DECLARE PLUGIN "g_eqdecide"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 54229bb2ae..fd33a779dc 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,6 +8,8 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
+DECLARE PLUGIN "ltac_plugin"
+
open Util
open Pp
open Compat
@@ -17,6 +19,7 @@ open Misctypes
open Genarg
open Genredexpr
open Tok (* necessary for camlp4 *)
+open Names
open Pcoq
open Pcoq.Constr
@@ -226,8 +229,8 @@ GEXTEND Gram
| "multimatch" -> General ] ]
;
input_fun:
- [ [ "_" -> None
- | l = ident -> Some l ] ]
+ [ [ "_" -> Anonymous
+ | l = ident -> Name l ] ]
;
let_clause:
[ [ id = identref; ":="; te = tactic_expr ->
@@ -499,8 +502,8 @@ let pr_tacdef_body tacdef_body =
| Tacexpr.TacFun (idl,b) -> idl,b
| _ -> [], body in
id ++
- prlist (function None -> str " _"
- | Some id -> spc () ++ Nameops.pr_id id) idl
+ prlist (function Anonymous -> str " _"
+ | Name id -> spc () ++ Nameops.pr_id id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
++ Pptactic.pr_raw_tactic body
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index d286a58708..3e6e2db605 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -70,7 +70,7 @@ GEXTEND Gram
Constr.closed_binder:
[[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" ->
let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in
- [LocalRawAssum ([id], default_binder_kind, typ)]
+ [CLocalAssum ([id], default_binder_kind, typ)]
] ];
END
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index b1c4f58eb8..c50100bf55 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
[ declare_relation a aeq n None None (Some lemma3) ]
END
-type binders_argtype = local_binder list
+type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 685c07c9a8..fa01baab75 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -325,8 +325,9 @@ GEXTEND Gram
l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] ->
let loc0,pat = pat in
let f c pat =
- let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in
- IntroAction (IntroApplyOn (c,(loc,pat))) in
+ let loc1 = Constrexpr_ops.constr_loc c in
+ let loc = Loc.merge loc0 loc1 in
+ IntroAction (IntroApplyOn ((loc1,c),(loc,pat))) in
!@loc, List.fold_right f l pat ] ]
;
simple_intropattern_closed:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index fccee6e40a..dc418d530e 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -27,6 +27,26 @@ open Pputils
open Ppconstr
open Printer
+module Tag =
+struct
+
+ let keyword = "tactic.keyword"
+ let primitive = "tactic.primitive"
+ let string = "tactic.string"
+
+end
+
+let tag t s = Pp.tag t s
+let do_not_tag _ x = x
+let tag_keyword = tag Tag.keyword
+let tag_primitive = tag Tag.primitive
+let tag_string = tag Tag.string
+let tag_glob_tactic_expr = do_not_tag
+let tag_glob_atomic_tactic_expr = do_not_tag
+let tag_raw_tactic_expr = do_not_tag
+let tag_raw_atomic_tactic_expr = do_not_tag
+let tag_atomic_tactic_expr = do_not_tag
+
let pr_global x = Nametab.pr_global_env Id.Set.empty x
type 'a grammar_tactic_prod_item_expr =
@@ -64,30 +84,6 @@ type 'a extra_genarg_printer =
(tolerability -> Val.t -> std_ppcmds) ->
'a -> std_ppcmds
-module Make
- (Ppconstr : Ppconstrsig.Pp)
- (Taggers : sig
- val tag_keyword
- : std_ppcmds -> std_ppcmds
- val tag_primitive
- : std_ppcmds -> std_ppcmds
- val tag_string
- : std_ppcmds -> std_ppcmds
- val tag_glob_tactic_expr
- : glob_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_glob_atomic_tactic_expr
- : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_raw_tactic_expr
- : raw_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_raw_atomic_tactic_expr
- : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- val tag_atomic_tactic_expr
- : atomic_tactic_expr -> std_ppcmds -> std_ppcmds
- end)
-= struct
-
- open Taggers
-
let keyword x = tag_keyword (str x)
let primitive x = tag_primitive (str x)
@@ -574,9 +570,7 @@ module Make
str "=>" ++ brk (1,4) ++ pr t))
| All t -> str "_" ++ spc () ++ str "=>" ++ brk (1,4) ++ pr t
- let pr_funvar = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
+ let pr_funvar n = spc () ++ pr_name n
let pr_let_clause k pr (id,(bl,t)) =
hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++
@@ -1208,37 +1202,6 @@ module Make
let pr_atomic_tactic env = pr_atomic_tactic_level env ltop
-end
-
-module Tag =
-struct
- let keyword =
- let style = Terminal.make ~bold:true () in
- Ppstyle.make ~style ["tactic"; "keyword"]
-
- let primitive =
- let style = Terminal.make ~fg_color:`LIGHT_GREEN () in
- Ppstyle.make ~style ["tactic"; "primitive"]
-
- let string =
- let style = Terminal.make ~fg_color:`LIGHT_RED () in
- Ppstyle.make ~style ["tactic"; "string"]
-
-end
-
-include Make (Ppconstr) (struct
- let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s
- let do_not_tag _ x = x
- let tag_keyword = tag Tag.keyword
- let tag_primitive = tag Tag.primitive
- let tag_string = tag Tag.string
- let tag_glob_tactic_expr = do_not_tag
- let tag_glob_atomic_tactic_expr = do_not_tag
- let tag_raw_tactic_expr = do_not_tag
- let tag_raw_atomic_tactic_expr = do_not_tag
- let tag_atomic_tactic_expr = do_not_tag
-end)
-
let declare_extra_genarg_pprule wit
(f : 'a raw_extra_genarg_printer)
(g : 'b glob_extra_genarg_printer)
@@ -1340,22 +1303,3 @@ let () =
let pr_unit _ _ _ () = str "()" in
let printer _ _ prtac = prtac (0, E) in
declare_extra_genarg_pprule wit_ltac printer printer pr_unit
-
-module Richpp = struct
-
- include Make (Ppconstr.Richpp) (struct
- open Ppannotation
- open Genarg
- let do_not_tag _ x = x
- let tag e s = Pp.tag (Pp.Tag.inj e tag) s
- let tag_keyword = tag AKeyword
- let tag_primitive = tag AKeyword
- let tag_string = do_not_tag ()
- let tag_glob_tactic_expr e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e))
- let tag_glob_atomic_tactic_expr = do_not_tag
- let tag_raw_tactic_expr e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e))
- let tag_raw_atomic_tactic_expr = do_not_tag
- let tag_atomic_tactic_expr = do_not_tag
- end)
-
-end
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 86e3ea5484..43e22dba3f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -13,6 +13,8 @@ open Pp
open Genarg
open Geninterp
open Names
+open Misctypes
+open Environ
open Constrexpr
open Tacexpr
open Ppextend
@@ -54,14 +56,66 @@ type pp_tactic = {
val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
-(** The default pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as raw strings. *)
-include Pptacticsig.Pp
+val pr_with_occurrences :
+ ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
+val pr_red_expr :
+ ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
+ ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
+val pr_may_eval :
+ ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
+
+val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
+val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+
+val pr_in_clause :
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_clauses : bool option ->
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
+val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
+
+val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
+
+val pr_raw_extend: env -> int ->
+ ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
+
+val pr_glob_extend: env -> int ->
+ ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
+
+val pr_extend :
+ (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
+
+val pr_alias_key : Names.KerName.t -> std_ppcmds
+
+val pr_alias : (Val.t -> std_ppcmds) ->
+ int -> Names.KerName.t -> Val.t list -> std_ppcmds
+
+val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
+
+val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
+
+val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
+
+val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
+
+val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
+
+val pr_hintbases : string list option -> std_ppcmds
+
+val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
+
+val pr_bindings :
+ ('constr -> std_ppcmds) ->
+ ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
+
+val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
+
+val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
+ ('b, 'a) match_rule -> std_ppcmds
+
+val pr_value : tolerability -> Val.t -> std_ppcmds
-(** The rich pretty-printers produce {!Pp.std_ppcmds} that are
- interpreted as annotated strings. The annotations can be
- retrieved using {!RichPp.rich_pp}. Their definitions are
- located in {!Ppannotation.t}. *)
-module Richpp : Pptacticsig.Pp
val ltop : tolerability
diff --git a/plugins/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli
deleted file mode 100644
index 74ddd377ad..0000000000
--- a/plugins/ltac/pptacticsig.mli
+++ /dev/null
@@ -1,81 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Pp
-open Genarg
-open Geninterp
-open Tacexpr
-open Ppextend
-open Environ
-open Misctypes
-
-module type Pp = sig
-
- val pr_with_occurrences :
- ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds
- val pr_red_expr :
- ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
- ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds
- val pr_may_eval :
- ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds
-
- val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
-
- val pr_in_clause :
- ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
- val pr_clauses : bool option ->
- ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
-
- val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds
-
- val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds
-
- val pr_raw_extend: env -> int ->
- ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds
-
- val pr_glob_extend: env -> int ->
- ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds
-
- val pr_extend :
- (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
-
- val pr_alias_key : Names.KerName.t -> std_ppcmds
-
- val pr_alias : (Val.t -> std_ppcmds) ->
- int -> Names.KerName.t -> Val.t list -> std_ppcmds
-
- val pr_alias_key : Names.KerName.t -> std_ppcmds
-
- val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
-
- val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
-
- val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds
-
- val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
-
- val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds
-
- val pr_hintbases : string list option -> std_ppcmds
-
- val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
-
- val pr_bindings :
- ('constr -> std_ppcmds) ->
- ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds
-
- val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds
-
- val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
- ('b, 'a) match_rule -> std_ppcmds
-
- val pr_value : tolerability -> Val.t -> std_ppcmds
-
-end
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 2514ededb0..58123f63ef 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -257,7 +257,7 @@ let string_of_call ck =
(Pptactic.pr_glob_tactic (Global.env ())
te)
) in
- for i = 0 to String.length s - 1 do if s.[i] = '\n' then s.[i] <- ' ' done;
+ let s = String.map (fun c -> if c = '\n' then ' ' else c) s in
let s = try String.sub s 0 (CString.string_index_from s 0 "(*") with Not_found -> s in
CString.strip s
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 35c4483513..4fdce0c84f 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -77,17 +77,17 @@ val is_applied_rewrite_relation :
env -> evar_map -> Context.Rel.t -> constr -> types option
val declare_relation :
- ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
+ ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
constr_expr option -> constr_expr option -> constr_expr option -> unit
val add_setoid :
- bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr ->
+ bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
Id.t -> unit
val add_morphism_infer : bool -> constr_expr -> Id.t -> unit
val add_morphism :
- bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit
+ bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..cd8c9e471e 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -302,9 +302,9 @@ let cons_production_parameter = function
| TacTerm _ -> None
| TacNonTerm (_, _, id) -> Some id
-let add_glob_tactic_notation local n prods forml ids tac =
+let add_glob_tactic_notation local ~level prods forml ids tac =
let parule = {
- tacgram_level = n;
+ tacgram_level = level;
tacgram_prods = prods;
} in
let tacobj = {
@@ -360,7 +360,7 @@ let extend_atomic_tactic name entries =
in
List.iteri add_atomic entries
-let add_ml_tactic_notation name prods =
+let add_ml_tactic_notation name ~level prods =
let len = List.length prods in
let iter i prods =
let open Tacexpr in
@@ -372,10 +372,12 @@ let add_ml_tactic_notation name prods =
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
let map id = Reference (Misctypes.ArgVar (Loc.ghost, id)) in
let tac = TacML (Loc.ghost, entry, List.map map ids) in
- add_glob_tactic_notation false 0 prods true ids tac
+ add_glob_tactic_notation false ~level prods true ids tac
in
List.iteri iter (List.rev prods);
- extend_atomic_tactic name prods
+ (** We call [extend_atomic_tactic] only for "basic tactics" (the ones at
+ tactic_expr level 0) *)
+ if Int.equal level 0 then extend_atomic_tactic name prods
(**********************************************************************)
(** Ltac quotations *)
@@ -504,10 +506,7 @@ let print_ltacs () =
| Tacexpr.TacFun (l, t) -> (l, t)
| _ -> ([], body)
in
- let pr_ltac_fun_arg = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
- in
+ let pr_ltac_fun_arg n = spc () ++ pr_name n in
hov 2 (pr_qualid qid ++ prlist pr_ltac_fun_arg l)
in
Feedback.msg_notice (prlist_with_sep fnl pr_entry entries)
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 969c118fb5..0695044736 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -45,7 +45,7 @@ val register_tactic_notation_entry : string -> ('a, 'b, 'c) Genarg.genarg_type -
to finding an argument by name (as in {!Genarg}) if there is none
matching. *)
-val add_ml_tactic_notation : ml_tactic_name ->
+val add_ml_tactic_notation : ml_tactic_name -> level:int ->
argument grammar_tactic_prod_item_expr list list -> unit
(** A low-level variant of {!add_tactic_notation} used by the TACTIC EXTEND
ML-side macro. *)
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 9c25a16457..e23992a807 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -282,7 +282,7 @@ constraint 'a = <
>
and 'a gen_tactic_fun_ast =
- Id.t option list * 'a gen_tactic_expr
+ Name.t list * 'a gen_tactic_expr
constraint 'a = <
term:'t;
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 4b5d87fc3c..3f83f104e9 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -248,8 +248,8 @@ and intern_intro_pattern_action lf ist = function
| IntroInjection l ->
IntroInjection (List.map (intern_intro_pattern lf ist) l)
| IntroWildcard | IntroRewrite _ as x -> x
- | IntroApplyOn (c,pat) ->
- IntroApplyOn (intern_constr ist c, intern_intro_pattern lf ist pat)
+ | IntroApplyOn ((loc,c),pat) ->
+ IntroApplyOn ((loc,intern_constr ist c), intern_intro_pattern lf ist pat)
and intern_or_and_intro_pattern lf ist = function
| IntroAndPattern l ->
@@ -646,7 +646,7 @@ and intern_tactic_or_tacarg ist = intern_tactic false ist
and intern_pure_tactic ist = intern_tactic true ist
and intern_tactic_fun ist (var,body) =
- let lfun = List.fold_left opt_cons ist.ltacvars var in
+ let lfun = List.fold_left name_cons ist.ltacvars var in
(var,intern_tactic_or_tacarg { ist with ltacvars = lfun } body)
and intern_tacarg strict onlytac ist = function
@@ -722,9 +722,7 @@ let split_ltac_fun = function
| TacFun (l,t) -> (l,t)
| t -> ([],t)
-let pr_ltac_fun_arg = function
- | None -> spc () ++ str "_"
- | Some id -> spc () ++ pr_id id
+let pr_ltac_fun_arg n = spc () ++ pr_name n
let print_ltac id =
try
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index fda9142eda..fe10f0c313 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -120,7 +120,7 @@ let combine_appl appl1 appl2 =
(* Values for interpretation *)
type tacvalue =
| VFun of appl*ltac_trace * value Id.Map.t *
- Id.t option list * glob_tactic_expr
+ Name.t list * glob_tactic_expr
| VRec of value Id.Map.t ref * glob_tactic_expr
let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) =
@@ -520,7 +520,7 @@ let rec intropattern_ids (loc,pat) = match pat with
List.flatten (List.map intropattern_ids (List.flatten ll))
| IntroAction (IntroInjection l) ->
List.flatten (List.map intropattern_ids l)
- | IntroAction (IntroApplyOn (c,pat)) -> intropattern_ids pat
+ | IntroAction (IntroApplyOn ((_,c),pat)) -> intropattern_ids pat
| IntroNaming (IntroAnonymous | IntroFresh _)
| IntroAction (IntroWildcard | IntroRewrite _)
| IntroForthcoming _ -> []
@@ -642,32 +642,32 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
Proofview.NonLogical.run (db_constr (curr_debug ist) env c);
(evd,c)
-let constr_flags = {
+let constr_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = true;
expand_evars = true }
(* 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
+ interp_gen kind ist false (constr_flags ()) env sigma c
let interp_constr = interp_constr_gen WithoutTypeConstraint
let interp_type = interp_constr_gen IsType
-let open_constr_use_classes_flags = {
+let open_constr_use_classes_flags () = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
-let open_constr_no_classes_flags = {
+let open_constr_no_classes_flags () = {
use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = Some solve_by_implicit_tactic;
+ use_hook = solve_by_implicit_tactic ();
fail_evar = false;
expand_evars = true }
@@ -679,11 +679,11 @@ let pure_open_constr_flags = {
expand_evars = false }
(* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist =
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
let flags =
- if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags
- else open_constr_use_classes_flags in
- interp_gen expected_type ist false flags
+ if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
+ else open_constr_use_classes_flags () in
+ interp_gen expected_type ist false flags env sigma c
let interp_pure_open_constr ist =
interp_gen WithoutTypeConstraint ist false pure_open_constr_flags
@@ -913,14 +913,14 @@ and interp_intro_pattern_action ist env sigma = function
| IntroInjection l ->
let sigma,l = interp_intro_pattern_list_as_list ist env sigma l in
sigma, IntroInjection l
- | IntroApplyOn (c,ipat) ->
+ | IntroApplyOn ((loc,c),ipat) ->
let c = { delayed = fun env sigma ->
let sigma = Sigma.to_evar_map sigma in
let (sigma, c) = interp_open_constr ist env sigma c in
Sigma.Unsafe.of_pair (c, sigma)
} in
let sigma,ipat = interp_intro_pattern ist env sigma ipat in
- sigma, IntroApplyOn (c,ipat)
+ sigma, IntroApplyOn ((loc,c),ipat)
| IntroWildcard | IntroRewrite _ as x -> sigma, x
and interp_or_and_intro_pattern ist env sigma = function
@@ -1087,8 +1087,8 @@ let head_with_value (lvar,lval) =
| ([],[]) -> (lacc,[],[])
| (vr::tvr,ve::tve) ->
(match vr with
- | None -> head_with_value_rec lacc (tvr,tve)
- | Some v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
+ | Anonymous -> head_with_value_rec lacc (tvr,tve)
+ | Name v -> head_with_value_rec ((v,ve)::lacc) (tvr,tve))
| (vr,[]) -> (lacc,vr,[])
| ([],ve) -> (lacc,[],ve)
in
@@ -1422,7 +1422,14 @@ and tactic_of_value ist vle =
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 _|VRec _) -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
+ | VFun (_, _, _,vars,_) ->
+ let numargs = List.length vars in
+ Tacticals.New.tclZEROMSG
+ (str "A fully applied tactic is expected:" ++ spc() ++ Pp.str "missing " ++
+ Pp.str (String.plural numargs "argument") ++ Pp.str " for " ++
+ Pp.str (String.plural numargs "variable") ++ Pp.str " " ++
+ pr_enum pr_name vars ++ Pp.str ".")
+ | VRec _ -> Tacticals.New.tclZEROMSG (str "A fully applied tactic is expected.")
else if has_type vle (topwit wit_tactic) then
let tac = out_gen (topwit wit_tactic) vle in
tactic_of_value ist tac
@@ -1780,7 +1787,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(TacLetTac(na,c,clp,b,eqpat))
(Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
(let_pat_tac b (interp_name ist env sigma na)
- ((sigma,sigma'),c) clp eqpat) sigma')
+ (sigma,c) clp eqpat) sigma')
end }
(* Derived basic tactics *)
@@ -2120,8 +2127,8 @@ let lift_constr_tac_to_ml_tac vars tac =
let env = Proofview.Goal.env gl in
let sigma = project gl in
let map = function
- | None -> None
- | Some id ->
+ | Anonymous -> None
+ | Name id ->
let c = Id.Map.find id ist.lfun in
try Some (coerce_to_closed_constr env c)
with CannotCoerceTo ty ->
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index 6f64981eff..adbd1d32be 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -115,7 +115,7 @@ val error_ltac_variable : Loc.t -> Id.t ->
(** Transforms a constr-expecting tactic into a tactic finding its arguments in
the Ltac environment according to the given names. *)
-val lift_constr_tac_to_ml_tac : Id.t option list ->
+val lift_constr_tac_to_ml_tac : Name.t list ->
(constr list -> Geninterp.interp_sign -> unit Proofview.tactic) -> Tacenv.ml_tactic
val default_ist : unit -> Geninterp.interp_sign
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b09bdda65c..fe3a9f3b2a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -51,8 +51,8 @@ let rec subst_intro_pattern subst = function
| loc, IntroNaming _ | loc, IntroForthcoming _ as x -> x
and subst_intro_pattern_action subst = function
- | IntroApplyOn (t,pat) ->
- IntroApplyOn (subst_glob_constr subst t,subst_intro_pattern subst pat)
+ | IntroApplyOn ((loc,t),pat) ->
+ IntroApplyOn ((loc,subst_glob_constr subst t),subst_intro_pattern subst pat)
| IntroOrAndPattern l ->
IntroOrAndPattern (subst_intro_or_and_pattern subst l)
| IntroInjection l -> IntroInjection (List.map (subst_intro_pattern subst) l)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 756958c2f0..fb05fd7d0e 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -259,7 +259,7 @@ let with_flags flags _ ist =
let register_tauto_tactic tac name0 args =
let ids = List.map (fun id -> Id.of_string id) args in
- let ids = List.map (fun id -> Some id) ids in
+ let ids = List.map (fun id -> Name id) ids in
let name = { mltac_plugin = tauto_plugin; mltac_tactic = name0; } in
let entry = { mltac_name = name; mltac_index = 0 } in
let () = Tacenv.register_ml_tactic name [| tac |] in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 15:45:26 +0000