aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--intf/tacexpr.mli17
-rw-r--r--parsing/egramcoq.ml5
-rw-r--r--parsing/egramcoq.mli1
-rw-r--r--printing/pptactic.ml4
-rw-r--r--tactics/tacenv.ml24
-rw-r--r--tactics/tacenv.mli21
-rw-r--r--tactics/tacintern.ml4
-rw-r--r--tactics/tacinterp.ml3
-rw-r--r--tactics/tacsubst.ml5
-rw-r--r--tactics/tactics.mllib1
-rw-r--r--toplevel/metasyntax.ml14
11 files changed, 28 insertions, 71 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 8f11fdbda..0ddf58b74 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -178,7 +178,8 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacExtend of Loc.t * string * 'lev generic_argument list
(* For syntax extensions *)
- | TacAlias of Loc.t * string * (Id.t * 'lev generic_argument) list
+ | TacAlias of Loc.t * string *
+ (Id.t * 'lev generic_argument) list * (DirPath.t * glob_tactic_expr)
(** Possible arguments of a tactic definition *)
@@ -249,14 +250,14 @@ and ('t,'p,'c,'i,'r,'n,'l) gen_tactic_fun_ast =
(** Globalized tactics *)
-type g_trm = glob_constr_and_expr
-type g_pat = glob_constr_and_expr * constr_pattern
-type g_cst = evaluable_global_reference and_short_name or_var
-type g_ind = inductive or_var
-type g_ref = ltac_constant located or_var
-type g_nam = Id.t located
+and g_trm = glob_constr_and_expr
+and g_pat = glob_constr_and_expr * constr_pattern
+and g_cst = evaluable_global_reference and_short_name or_var
+and g_ind = inductive or_var
+and g_ref = ltac_constant located or_var
+and g_nam = Id.t located
-type glob_tactic_expr =
+and glob_tactic_expr =
(g_trm, g_pat, g_cst, g_ind, g_ref, g_nam, glevel) gen_tactic_expr
type glob_atomic_tactic_expr =
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 669370890..34e0dcdef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -249,6 +249,7 @@ type tactic_grammar = {
tacgram_key : string;
tacgram_level : int;
tacgram_prods : grammar_prod_item list;
+ tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
}
type all_grammar_command =
@@ -268,12 +269,12 @@ let add_tactic_entry tg =
if not (head_is_ident tg) then
error "Notation for simple tactic must start with an identifier.";
let mkact loc l =
- (TacAlias (loc,tg.tacgram_key,l):raw_atomic_tactic_expr) in
+ (TacAlias (loc,tg.tacgram_key,l,tg.tacgram_tactic):raw_atomic_tactic_expr) in
make_rule mkact tg.tacgram_prods
end
else
let mkact loc l =
- (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l)):raw_tactic_expr) in
+ (TacAtom(loc,TacAlias(loc,tg.tacgram_key,l,tg.tacgram_tactic)):raw_tactic_expr) in
make_rule mkact tg.tacgram_prods in
synchronize_level_positions ();
grammar_extend entry None (Option.map of_coq_position pos,[(None, None, List.rev [rules])]);
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 5953eb0f8..9ae49f718 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -44,6 +44,7 @@ type tactic_grammar = {
tacgram_key : string;
tacgram_level : int;
tacgram_prods : grammar_prod_item list;
+ tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
}
(** {5 Adding notations} *)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0bb9982c2..2ce3eba06 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -623,7 +623,7 @@ let rec pr_atom0 = function
and pr_atom1 = function
| TacExtend (loc,s,l) ->
pr_with_comments loc (pr_extend 1 s l)
- | TacAlias (loc,s,l) ->
+ | TacAlias (loc,s,l,_) ->
pr_with_comments loc (pr_extend 1 s (List.map snd l))
(* Basic tactics *)
@@ -912,7 +912,7 @@ let rec pr_tac inherited tac =
pr_tac (lcomplete,E) t, lcomplete
| TacId l ->
str "idtac" ++ prlist (pr_arg (pr_message_token pr_ident)) l, latom
- | TacAtom (loc,TacAlias (_,s,l)) ->
+ | TacAtom (loc,TacAlias (_,s,l,_)) ->
pr_with_comments loc
(pr_extend (level_of inherited) s (List.map snd l)),
latom
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
deleted file mode 100644
index 27ab5ab95..000000000
--- a/tactics/tacenv.ml
+++ /dev/null
@@ -1,24 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Util
-open Pp
-open Names
-open Tacexpr
-
-type alias = string
-
-let alias_map = Summary.ref ~name:"tactic-alias"
- (String.Map.empty : (DirPath.t * glob_tactic_expr) String.Map.t)
-
-let register_alias key dp tac =
- alias_map := String.Map.add key (dp, tac) !alias_map
-
-let interp_alias key =
- try String.Map.find key !alias_map
- with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ str key)
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
deleted file mode 100644
index ba3bd8a28..000000000
--- a/tactics/tacenv.mli
+++ /dev/null
@@ -1,21 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-open Names
-open Tacexpr
-
-(** This module centralizes the various ways of registering tactics. *)
-
-type alias = string
-(** Type of tactic alias, used in the [TacAlias] node. *)
-
-val register_alias : alias -> DirPath.t -> glob_tactic_expr -> unit
-(** Register a tactic alias. *)
-
-val interp_alias : alias -> (DirPath.t * glob_tactic_expr)
-(** Recover the the body of an alias. *)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index edbec7a04..42ea649ec 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -634,9 +634,9 @@ let rec intern_atomic lf ist x =
| TacExtend (loc,opn,l) ->
!assert_tactic_installed opn;
TacExtend (adjust_loc loc,opn,List.map (intern_genarg ist) l)
- | TacAlias (loc,s,l) ->
+ | TacAlias (loc,s,l,(dir,body)) ->
let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
- TacAlias (loc,s,l)
+ TacAlias (loc,s,l,(dir,body))
and intern_tactic onlytac ist tac = snd (intern_tactic_seq onlytac ist tac)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 39f3a20f1..248a5d36b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2231,8 +2231,7 @@ and interp_atomic ist tac =
Proofview.V82.tclEVARS sigma <*>
tac args ist
end
- | TacAlias (loc,s,l) ->
- let (_, body) = Tacenv.interp_alias s in
+ | TacAlias (loc,s,l,(_,body)) ->
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let rec f x =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index d6e17363a..7c968865a 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -219,8 +219,9 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
(* For extensions *)
| TacExtend (_loc,opn,l) ->
TacExtend (dloc,opn,List.map (subst_genarg subst) l)
- | TacAlias (_,s,l) ->
- TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l)
+ | TacAlias (_,s,l,(dir,body)) ->
+ TacAlias (dloc,s,List.map (fun (id,a) -> (id,subst_genarg subst a)) l,
+ (dir,subst_tactic subst body))
and subst_tactic subst (t:glob_tactic_expr) = match t with
| TacAtom (_loc,t) -> TacAtom (dloc, subst_atomic subst t)
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index f1227c234..7b91665ad 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -15,7 +15,6 @@ Equality
Contradiction
Inv
Leminv
-Tacenv
Tacsubst
Taccoerce
Tacintern
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index b882cc8ec..4bce9b73e 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -65,19 +65,19 @@ type tactic_grammar_obj = {
tacobj_local : locality_flag;
tacobj_tacgram : tactic_grammar;
tacobj_tacpp : Pptactic.pp_tactic;
- tacobj_body : DirPath.t * Tacexpr.glob_tactic_expr
}
let cache_tactic_notation (_, tobj) =
- let key = tobj.tacobj_tacgram.tacgram_key in
- let (dp, body) = tobj.tacobj_body in
- Tacenv.register_alias key dp body;
Egramcoq.extend_tactic_grammar tobj.tacobj_tacgram;
Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp
+let subst_tactic_parule subst tg =
+ let dir, tac = tg.tacgram_tactic in
+ { tg with tacgram_tactic = (dir, Tacsubst.subst_tactic subst tac); }
+
let subst_tactic_notation (subst, tobj) =
- let dir, tac = tobj.tacobj_body in
- { tobj with tacobj_body = (dir, Tacsubst.subst_tactic subst tac) }
+ { tobj with
+ tacobj_tacgram = subst_tactic_parule subst tobj.tacobj_tacgram; }
let classify_tactic_notation tacobj =
if tacobj.tacobj_local then Dispose else Substitute tacobj
@@ -117,12 +117,12 @@ let add_tactic_notation (local,n,prods,e) =
tacgram_key = key;
tacgram_level = n;
tacgram_prods = prods;
+ tacgram_tactic = (Lib.cwd (), tac);
} in
let tacobj = {
tacobj_local = local;
tacobj_tacgram = parule;
tacobj_tacpp = pprule;
- tacobj_body = (Lib.cwd (), tac);
} in
Lib.add_anonymous_leaf (inTacticGrammar tacobj)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 21:58:25 +0000