diff options
| author | letouzey | 2012-10-06 10:08:45 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-06 10:08:45 +0000 |
| commit | e1bdb515ee2f701bfc56f1bcf4a8e404f759a38a (patch) | |
| tree | 52eb681313f840b3d46d633ed0440e3ad96ace9a /grammar | |
| parent | f975575187d0a19e7cc1afc43459a92eeb12b3f1 (diff) | |
remove Refiner.abstract_tactic and similar
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 8b5b64ffc2..5500a233a3 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -174,12 +174,7 @@ let declare_tactic loc s cl = let hide_tac (p,e) = (* reste a definir les fonctions cachees avec des noms frais *) let stac = "h_"^s in - let e = - make_fun - <:expr< - Refiner.abstract_extended_tactic $make_eval_tactic e p$ - >> - p in + let e = make_fun (make_eval_tactic e p) p in <:str_item< value $lid:stac$ = $e$ >> in let hidden = if List.length cl = 1 then List.map hide_tac cl else [] in |