diff options
| -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 2a2db30f83..4aace33dcf 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 d90de63c94..3e00990105 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 |