From a84797db94e9d242ebdf9f6feb08a63d42a14bae Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 24 Feb 2017 00:27:50 +0100
Subject: TACTIC EXTEND now takes an optional level as argument.

The syntax is: TACTIC EXTEND foo AT LEVEL i

This commit makes it possible to define tacticals like the ssreflect
arrow without having to resort to GEXTEND statements and intepretation
hacks.

Note that it simply makes accessible through the ML interface what Tactic
Notation already supports:

Tactic Notation (at level 1) tactic1(t) "=>" ipats(l) := ...
---
 plugins/ltac/tacentries.ml  | 12 +++++++-----
 plugins/ltac/tacentries.mli |  2 +-
 2 files changed, 8 insertions(+), 6 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 2e2b55be74..8570b5a447 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                                                   *)
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. *)
-- 
cgit v1.2.3