diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-08 20:26:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-11-08 20:26:44 +0000 |
| commit | 96bf275ab400c60989893cf62e3638c057feb26e (patch) | |
| tree | 6d14194f72d07cf299d2f84761a7ced0866ac3ac | |
| parent | ba1981f71e84895c32d9afd4c23bf6e81863e1f4 (diff) | |
Code obsolete
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4833 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/extraargs.ml4 | 18 | ||||
| -rw-r--r-- | tactics/extraargs.mli | 4 |
2 files changed, 1 insertions, 21 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 2a2db30f8..4aace33dc 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -28,20 +28,4 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient | [ "<-" ] -> [ false ] | [ ] -> [ true ] END - -(* with_constr *) - -open Tacinterp - -let pr_with_constr_gen prc _prtac = function - | None -> Pp.mt () - | Some c -> Pp.str " with" ++ prc c - -ARGUMENT EXTEND with_constr - TYPED AS constr_opt - PRINTED BY pr_with_constr_gen - INTERPRETED BY interp_genarg - GLOBALIZED BY intern_genarg -| [ "with" constr(c) ] -> [ Some c ] -| [ ] -> [ None ] -END + diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index d90de63c9..3e0099010 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -16,7 +16,3 @@ open Topconstr val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool closed_abstract_argument_type val orient : bool Pcoq.Gram.Entry.e - -val rawwit_with_constr : constr_expr option raw_abstract_argument_type -val wit_with_constr : constr option closed_abstract_argument_type -val with_constr : constr_expr option Pcoq.Gram.Entry.e |