From ac630f12c9d80c9387d44f3f1a1b22db5b5b89da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 22 Dec 2016 13:48:01 +0100
Subject: Fixing anomaly EqUnknown in Equality Scheme (#5278).

---
 toplevel/auto_ind_decl.ml | 18 +++++++++---------
 toplevel/indschemes.ml    |  3 +++
 2 files changed, 12 insertions(+), 9 deletions(-)

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b3144fa927..a527be32ba 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -204,19 +204,19 @@ let build_beq_scheme mode kn =
             end
         | Sort _  -> raise InductiveWithSort
         | Prod _ -> raise InductiveWithProduct
-        | Lambda _-> raise (EqUnknown "Lambda")
-        | LetIn _ -> raise (EqUnknown "LetIn")
+        | Lambda _-> raise (EqUnknown "abstraction")
+        | LetIn _ -> raise (EqUnknown "let-in")
         | Const kn ->
 	    (match Environ.constant_opt_value_in env kn with
 	      | None -> raise (ParameterWithoutEquality (fst kn))
 	      | Some c -> aux (applist (c,a)))
-        | Proj _ -> raise (EqUnknown "Proj")
-        | Construct _ -> raise (EqUnknown "Construct")
-        | Case _ -> raise (EqUnknown "Case")
-        | CoFix _ -> raise (EqUnknown "CoFix")
-        | Fix _   -> raise (EqUnknown "Fix")
-        | Meta _  -> raise (EqUnknown "Meta")
-        | Evar _  -> raise (EqUnknown "Evar")
+        | Proj _ -> raise (EqUnknown "projection")
+        | Construct _ -> raise (EqUnknown "constructor")
+        | Case _ -> raise (EqUnknown "match")
+        | CoFix _ -> raise (EqUnknown "cofix")
+        | Fix _   -> raise (EqUnknown "fix")
+        | Meta _  -> raise (EqUnknown "meta-variable")
+        | Evar _  -> raise (EqUnknown "existential variable")
     in
       aux t
   in
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index aa2362ae5f..0e59f1aa98 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -185,6 +185,9 @@ let try_declare_scheme what f internal names kn =
     | DecidabilityMutualNotSupported ->
         alarm what internal
           (str "Decidability lemma for mutual inductive types not supported.")
+    | EqUnknown s ->
+         alarm what internal
+           (str "Found unsupported " ++ str s ++ str " while building Boolean equality.")
     | e when Errors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
-- 
cgit v1.2.3