From cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Sun, 1 Feb 2009 00:54:40 +0100
Subject: Imported Upstream version 8.2~rc2+dfsg

---
 tactics/extraargs.ml4 | 21 +++------------------
 1 file changed, 3 insertions(+), 18 deletions(-)

(limited to 'tactics/extraargs.ml4')

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index a0230b28..694c3495 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extraargs.ml4 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: extraargs.ml4 11800 2009-01-18 18:34:15Z msozeau $ *)
 
 open Pp
 open Pcoq
@@ -16,6 +16,7 @@ open Genarg
 open Names
 open Tacexpr
 open Tacinterp
+open Termops
 
 (* Rewriting orientation *)
 
@@ -97,22 +98,6 @@ ARGUMENT EXTEND occurrences
 | [ var(id) ] -> [ ArgVar id ]
 END
 
-(* For Setoid rewrite *)
-let pr_morphism_signature _ _ _ s =
-  spc () ++ Setoid_replace.pr_morphism_signature s
-
-ARGUMENT EXTEND morphism_signature
- TYPED AS morphism_signature
- PRINTED BY pr_morphism_signature
-  | [ constr(out) ] -> [ [],out ]
-  | [ constr(c) "++>" morphism_signature(s) ] ->
-       [ let l,out = s in (Some true,c)::l,out ]
-  | [ constr(c) "-->" morphism_signature(s) ] ->
-       [ let l,out = s in (Some false,c)::l,out ]
-  | [ constr(c) "==>" morphism_signature(s) ] ->
-       [ let l,out = s in (None,c)::l,out ]
-END
-
 let pr_gen prc _prlc _prtac c = prc c
 
 let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
@@ -288,7 +273,7 @@ let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause =
    Option.map 
      (fun l -> 
 	List.map 
-	  (fun id -> ( (all_occurrences_expr,trad_id id) ,Tacexpr.InHyp))
+	  (fun id -> ( (all_occurrences_expr,trad_id id),InHyp))
 	  l
      )
      hyps;
-- 
cgit v1.2.3