The Prod special case works only when the premise is of type Prop.

This is now checked.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6156 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 13 insertions, 2 deletions

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 4045816eb..9c10ce51c 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1058,8 +1058,19 @@ let mark_occur gl t in_c input_relation input_direction =
             (str "Cannot rewrite in the type of a variable bound " ++
              str "in a dependent product.")
           else 
-           aux output_relation output_direction
-            (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
+           let typeofc1 = Tacmach.pf_type_of gl c1 in
+            if not (Tacmach.pf_conv_x gl typeofc1 mkProp) then
+             (* to avoid this error we should introduce an impl relation
+                whose first argument is Type instead of Prop *)
+             errorlabstrm "Setoid_replace"
+              (str "Rewriting in a product A -> B is possible only when A " ++
+               str "is a proposition (i.e. A is of type Prop). The type " ++
+               prterm c1 ++ str " has type " ++ prterm typeofc1 ++
+               str " that is not convertible to Prop. If you need this " ++
+               str "feature, please ask the author.")
+            else
+             aux output_relation output_direction
+              (mkApp ((Lazy.force coq_impl), [| c1 ; c2 |]))
       | _ -> [ToKeep (in_c,output_relation,output_direction)]
  in
   let aux2 output_relation output_direction =