From cb6c3ec2e66e3019cb9ee881b1e222e6e3691463 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Jul 2015 10:50:04 +0200
Subject: Fixing bug #3736 (anomaly instead of error/warning/silence on
 decidability scheme).

Not clear to me why it is not a warning (in verbose mode) rather than
silence when a scheme supposed to be built automatically cannot be
built, as in:

Set Decidable Equality Schemes.
Inductive a := A with b := B.

which could explain why a_beq and a_eq_dec as well as b_beq and
b_eq_dec are not built.
---
 test-suite/bugs/closed/3736.v | 8 ++++++++
 toplevel/auto_ind_decl.ml     | 3 ++-
 toplevel/auto_ind_decl.mli    | 1 +
 toplevel/indschemes.ml        | 3 +++
 4 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/3736.v

diff --git a/test-suite/bugs/closed/3736.v b/test-suite/bugs/closed/3736.v
new file mode 100644
index 0000000000..637b77cc58
--- /dev/null
+++ b/test-suite/bugs/closed/3736.v
@@ -0,0 +1,8 @@
+(* Check non-error failure in case of unsupported decidability scheme *)
+Local Set Decidable Equality Schemes.
+
+Inductive a := A with b := B.
+
+(* But fails with error if explicitly asked for the scheme *)
+
+Fail Scheme Equality for a.
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f905080905..d1452fca21 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -55,6 +55,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 let dl = Loc.ghost
 
@@ -921,7 +922,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
 let make_eq_decidability mind =
   let mib = Global.lookup_mind mind in
   if not (Int.equal (Array.length mib.mind_packets) 1) then
-    anomaly (Pp.str "Decidability lemma for mutual inductive types not supported");
+    raise DecidabilityMutualNotSupported;
   let ind = (mind,0) in
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 807872988b..20a3d5d74f 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -23,6 +23,7 @@ exception InductiveWithProduct
 exception InductiveWithSort
 exception ParameterWithoutEquality of constant
 exception NonSingletonProp of inductive
+exception DecidabilityMutualNotSupported
 
 val beq_scheme_kind : mutual scheme_kind
 val build_beq_scheme : mutual_scheme_object_function
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index fbc45b4ae3..f8f062dad6 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -180,6 +180,9 @@ let try_declare_scheme what f internal names kn =
 	  (strbrk "Required constant " ++ str s ++ str " undefined.")
     | AlreadyDeclared msg ->
         alarm what internal (msg ++ str ".")
+    | DecidabilityMutualNotSupported ->
+        alarm what internal
+          (str "Decidability lemma for mutual inductive types not supported.")
     | e when Errors.noncritical e ->
 	alarm what internal
 	  (str "Unknown exception during scheme creation: "++
-- 
cgit v1.2.3