Globalisation des Tactic Notation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 1 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2dc20dced..71a35edcc 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -199,7 +199,14 @@ let add_grammar_obj univ entryl =
 
 (* Tactic notations *)
 
-let locate_tactic_body dir (s,p,e) = (s,p,(dir,e))
+let cons_production_parameter l = function
+  | VTerm _ -> l
+  | VNonTerm (_,_,ido) -> option_cons ido l
+
+let locate_tactic_body dir (s,(_,prods as p),e) = 
+  let ids = List.fold_left cons_production_parameter [] prods in
+  let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
+  (s,p,(dir,tac))
 
 let add_tactic_grammar g =
   let dir = Lib.cwd () in