diff options
-rw-r--r-- | test-suite/bugs/closed/6951.v | 2 | ||||
-rw-r--r-- | vernac/auto_ind_decl.ml | 12 |
2 files changed, 12 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/6951.v b/test-suite/bugs/closed/6951.v new file mode 100644 index 000000000..419f8d7c4 --- /dev/null +++ b/test-suite/bugs/closed/6951.v @@ -0,0 +1,2 @@ +Record float2 : Set := Float2 { Fnum : unit }. +Scheme Equality for float2. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 3de7fe06b..30a268a11 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -319,9 +319,17 @@ 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 = CoFinite then + let fix = match mib.mind_finite with + | CoFinite -> raise NoDecidabilityCoInductive; - let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in + | Finite -> + mkFix (((Array.make nb_ind 0),i),(names,types,cores)) + | BiFinite -> + (** If the inductive type is not recursive, the fixpoint is not + used, so let's replace it with garbage *) + let subst = List.init nb_ind (fun _ -> mkProp) in + Vars.substl subst cores.(i) + in create_input fix), UState.make (Global.universes ())), !eff |