From 50fa3c5983fd630e56f34b55729d194181feef18 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Mon, 18 Oct 2004 15:00:29 +0000
Subject: The lem field was not computed properly for morphisms whose argument
 was a quantified Leibniz relation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6236 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index a1b6f97c72..19ab45105b 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -248,7 +248,7 @@ let prrelation_class =
        (*CSC: still "setoid" in the error message *)
        str "[[ Error: setoid on equality " ++ prterm eq ++ str " not found! ]]")
   | Leibniz (Some ty) -> prterm ty
-  | Leibniz None -> str "?"
+  | Leibniz None -> str "_"
 
 let prmorphism_argument_gen prrelation (variance,rel) =
  prrelation rel ++
@@ -677,7 +677,12 @@ let add_morphism lemma_infos mor_name (m,quantifiers_rev,args,output) =
         List.map
          (fun (v,rel) ->
            match rel with
-              Leibniz t -> v, Leibniz t
+              Leibniz (Some t) ->
+               assert (subst=[||]);
+               v, Leibniz (Some t)
+            | Leibniz None ->
+               assert (Array.length subst = 1);
+               v, Leibniz (Some (subst.(0)))
             | Relation rel -> v, Relation (apply_to_relation subst rel)) args
       in
        compose_lam quantifiers_rev
-- 
cgit v1.2.3