From 72b9a7df489ea47b3e5470741fd39f6100d31676 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Sat, 18 Aug 2007 20:34:57 +0000
Subject: Imported Upstream version 8.1.pl1+dfsg

---
 tactics/setoid_replace.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'tactics/setoid_replace.ml')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 2727e669..c14462eb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: setoid_replace.ml 9331 2006-11-01 09:36:06Z herbelin $ *)
+(* $Id: setoid_replace.ml 9853 2007-05-23 14:25:47Z letouzey $ *)
 
 open Tacmach
 open Proof_type
@@ -709,9 +709,10 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
 let unify_relation_carrier_with_type env rel t =
  let raise_error quantifiers_no =
   errorlabstrm "New Morphism"
-   (str "One morphism argument or its output has type " ++ pr_lconstr t ++
+   (str "One morphism argument or its output has type " ++ 
+    pr_lconstr_env env t ++
     str " but the signature requires an argument of type \"" ++
-    pr_lconstr rel.rel_a ++ str " " ++ prvect_with_sep pr_spc (fun _ -> str  "?")
+    pr_lconstr_env env rel.rel_a ++ prvect_with_sep mt (fun _ -> str " ?")
      (Array.make quantifiers_no 0) ++ str "\"") in
  let args =
   match kind_of_term t with
@@ -757,9 +758,10 @@ let unify_relation_class_carrier_with_type env rel t =
       rel
      else
       errorlabstrm "New Morphism"
-       (str "One morphism argument or its output has type " ++ pr_lconstr t ++
+       (str "One morphism argument or its output has type " ++ 
+        pr_lconstr_env env t ++
         str " but the signature requires an argument of type " ++
-        pr_lconstr t')
+        pr_lconstr_env env t')
   | Leibniz None -> Leibniz (Some t)
   | Relation rel -> Relation (unify_relation_carrier_with_type env rel t)
 
@@ -961,6 +963,8 @@ let new_named_morphism id m sign =
   match sign with
      None -> None
    | Some (args,out) ->
+      if args = [] then
+	error "Morphism signature expects at least one argument.";
       Some
        (List.map (fun (variance,ty) -> variance, constr_of ty) args,
         constr_of out)
@@ -1947,7 +1951,7 @@ let setoid_reflexivity gl =
            (str "The relation " ++ prrelation rel ++ str " is not reflexive.")
        | Some refl -> apply refl gl
  with
-  Optimize -> reflexivity gl
+  Optimize -> reflexivity_red true gl
 
 let setoid_symmetry gl =
  try
@@ -1963,7 +1967,7 @@ let setoid_symmetry gl =
            (str "The relation " ++ prrelation rel ++ str " is not symmetric.")
        | Some sym -> apply sym gl
  with
-  Optimize -> symmetry gl
+  Optimize -> symmetry_red true gl
 
 let setoid_symmetry_in id gl =
  let new_hyp =
@@ -1998,7 +2002,7 @@ let setoid_transitivity c gl =
             apply_with_bindings
              (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
  with
-  Optimize -> transitivity c gl
+  Optimize -> transitivity_red true c gl
 ;;
 
 Tactics.register_setoid_reflexivity setoid_reflexivity;;
-- 
cgit v1.2.3