diff options
| author | gareuselesinge | 2013-05-29 13:21:00 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-05-29 13:21:00 +0000 |
| commit | 9b3c26ae23606ceab42a44b5f9aa9d169016e564 (patch) | |
| tree | cfda25b8a3e2d0c2e3f63eeb34115deea6fed594 /grammar | |
| parent | 18373e78c9a0f171f193605ccb2556bb064b6e62 (diff) | |
Make ist (interp_sign) available to TACTIC EXTEND code
In order to do so I had to move the data base of tactics to
tacinterp (from tacintern).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16540 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 2972651a9e..6e62504a3c 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -38,7 +38,7 @@ let rec make_when loc = function | _::l -> make_when loc l let rec make_let e = function - | [] -> e + | [] -> <:expr< fun $lid:"ist"$ -> $e$ >> | GramNonTerminal(loc,t,_,Some p)::l -> let loc = of_coqloc loc in let p = Names.Id.to_string p in @@ -159,7 +159,7 @@ let declare_tactic loc s cl = declare_str_items loc [ <:str_item< do { try - let _=Tacintern.add_tactic $se$ $make_fun_clauses loc s cl$ in + let _=Tacinterp.add_tactic $se$ $make_fun_clauses loc s cl$ in List.iter (fun (s,l) -> match l with [ Some l -> |