diff options
| author | letouzey | 2012-04-23 18:51:11 +0000 |
|---|---|---|
| committer | letouzey | 2012-04-23 18:51:11 +0000 |
| commit | 7e02b97b3017a5a3055fca8e0fc6e89f84b6a1c4 (patch) | |
| tree | 1009560f396c397caa537471fc922aa0fb2af0bf /parsing | |
| parent | e3567014035a55cfde44099ce59d142d084faac5 (diff) | |
remove undocumented and scarcely-used tactic auto decomp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_tactic.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pptactic.ml | 4 |
2 files changed, 0 insertions, 8 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ddff97128e..79783fd3fa 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -610,10 +610,6 @@ GEXTEND Gram | d = trivial; lems = auto_using; db = hintbases -> TacTrivial (d,lems,db) | d = auto; n = OPT int_or_var; lems = auto_using; db = hintbases -> TacAuto (d,n,lems,db) - | d = auto; IDENT "decomp"; p = OPT natural; lems = auto_using -> - TacDAuto (d,None,p,lems) - | d = auto; n = OPT int_or_var; IDENT "decomp"; p = OPT natural; - lems = auto_using -> TacDAuto (d,n,p,lems) (* Context management *) | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacClear (true, l) diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c4c8579d95..5130341947 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -748,10 +748,6 @@ and pr_atom1 = function hov 0 (str (string_of_debug d ^ "auto") ++ pr_opt (pr_or_var int) n ++ pr_auto_using pr_constr lems ++ pr_hintbases db) - | TacDAuto (d,n,p,lems) -> - hov 1 (str (string_of_debug d ^ "auto") ++ - pr_opt (pr_or_var int) n ++ str "decomp" ++ - pr_opt int p ++ pr_auto_using pr_constr lems) (* Context management *) | TacClear (true,[]) as t -> pr_atom0 t |