Merge branch 'v8.6'

4 files changed, 23 insertions, 11 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f4b0b1b776..594f2e9449 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -58,6 +58,7 @@ exception InductiveWithSort
 exception ParameterWithoutEquality of global_reference
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
+exception NoDecidabilityCoInductive
 
 let dl = Loc.ghost
 
@@ -212,19 +213,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 (ConstRef (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
@@ -309,6 +310,8 @@ let build_beq_scheme mode kn =
       let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
 	if not (Sorts.List.mem InSet kelim) then
 	  raise (NonSingletonProp (kn,i));
+        if mib.mind_finite = Decl_kinds.CoFinite then
+	  raise NoDecidabilityCoInductive;
         let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
         create_input fix),
        Evd.make_evar_universe_context (Global.env ()) None),
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index fa5c61484e..60232ba8f4 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -24,6 +24,7 @@ exception InductiveWithSort
 exception ParameterWithoutEquality of Globnames.global_reference
 exception NonSingletonProp of inductive
 exception DecidabilityMutualNotSupported
+exception NoDecidabilityCoInductive
 
 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 48521a8e5d..f7e3f0d954 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -186,6 +186,12 @@ 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.")
+    | NoDecidabilityCoInductive ->
+         alarm what internal
+           (str "Scheme Equality is only for inductive types.")
     | e when CErrors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ CErrors.print e)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 76de9d7adb..d5faafaf89 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -552,8 +552,10 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
     | _ -> acc in
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
-  if not (List.distinct_f Id.compare allnames)
-  then error "Two objects have the same name";
+  let () = match List.duplicates Id.equal allnames with
+  | [] -> ()
+  | id :: _ -> user_err (str "Two objects have the same name" ++ spc () ++ quote (Id.print id))
+  in
   let isnot_class = match kind with Class false -> false | _ -> true in
   if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
     error "Priorities only allowed for type class substructures";