diff options
| -rw-r--r-- | tactics/setoid_replace.ml | 15 |
1 files changed, 13 insertions, 2 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 4045816eba..9c10ce51c0 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 = |