diff options
| -rw-r--r-- | parsing/egrammar.ml | 2 | ||||
| -rw-r--r-- | parsing/egrammar.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 9 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
7 files changed, 20 insertions, 5 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 4b7659caf..9983671e3 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -28,7 +28,7 @@ type all_grammar_command = | Grammar of grammar_command | TacticGrammar of (string * (string * grammar_production list) * - (Names.dir_path * Tacexpr.raw_tactic_expr)) + (Names.dir_path * Tacexpr.glob_tactic_expr)) list let subst_all_grammar_command subst = function diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli index e8292bf05..cee0a1ea9 100644 --- a/parsing/egrammar.mli +++ b/parsing/egrammar.mli @@ -28,7 +28,7 @@ type all_grammar_command = | Grammar of grammar_command | TacticGrammar of (string * (string * grammar_production list) * - (Names.dir_path * Tacexpr.raw_tactic_expr)) + (Names.dir_path * Tacexpr.glob_tactic_expr)) list val extend_grammar : all_grammar_command -> unit diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 76b99925a..16dcc65ea 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2215,6 +2215,12 @@ let add_tacdef isrec tacl = let glob_tactic x = intern_tactic (make_empty_glob_sign ()) x let glob_tactic_env l env x = + Options.with_option strict_check + (intern_tactic + { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env }) + x + +let glob_tactic_env_v7 l env x = intern_tactic { ltacvars = (l,[]); ltacrecvars = []; gsigma = Evd.empty; genv = env } x diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index a1ad99dfa..83b0d7acd 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -119,6 +119,8 @@ val glob_tactic : raw_tactic_expr -> glob_tactic_expr val glob_tactic_env : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr +val glob_tactic_env_v7 : identifier list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr + val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic 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) diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 6bea86fec..985280cfd 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -94,7 +94,7 @@ let pr_gen env t = (Pptacticnew.pr_raw_tactic env) pr_reference t let pr_raw_tactic tac = - pr_raw_tactic_env [] (Global.env()) tac + Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac) let rec extract_signature = function | [] -> [] |