Fix #6951: Unexpected error during scheme creation.

When creating a scheme for bifinite inductive types, we do not create a
fixpoint.

1 files changed, 10 insertions, 2 deletions

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