diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-05-30 16:44:56 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-30 16:44:56 +0200 |
commit | 3440a9fcc0690b66ff57a693b61dd6ccb13582c0 (patch) | |
tree | cbdc56e553e3d6f4a9d56a679f000f43570ed1a5 /vernac | |
parent | b75f714c025b51ed8b4db15bfce99df2d6ae7c41 (diff) | |
parent | 0ab081179fc448286c4cb0e9fcd4f67c37ed964c (diff) |
Merge PR #7260: Fix #6951: Unexpected error during scheme creation.
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/auto_ind_decl.ml | 12 |
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 |