diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-15 14:36:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-05-15 14:36:07 +0000 |
| commit | 9283721b945049795204f0e0e123bbb163a3d1c4 (patch) | |
| tree | 26e63c81ad0ff221ee92b92d851451aa1499eb0f /toplevel | |
| parent | b5006764caad04e464a27ea7fb585ddc82d48c17 (diff) | |
Globalisation des Tactic Notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7022 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
2 files changed, 9 insertions, 2 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 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 6cdbfaf20..ea9bce69e 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -123,7 +123,7 @@ let pre_printing = function (try let (_,env) = Pfedit.get_goal_context i in let t = Options.with_option Options.translate_syntax - (Tacinterp.glob_tactic_env [] env) tac in + (Tacinterp.glob_tactic_env_v7 [] env) tac in let pfts = Pfedit.get_pftreestate () in let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in Some (env,t,Pfedit.focus(),List.length gls) |