From 96bf275ab400c60989893cf62e3638c057feb26e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 8 Nov 2003 20:26:44 +0000
Subject: Code obsolete

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4833 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extraargs.ml4 | 18 +-----------------
 tactics/extraargs.mli |  4 ----
 2 files changed, 1 insertion(+), 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
-- 
cgit v1.2.3