diff options
| author | Hugo Herbelin | 2016-12-23 11:53:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2016-12-23 11:53:44 +0100 |
| commit | 3b821bf60d89c386c27487e172e57a669b5c4662 (patch) | |
| tree | 20da642d2c626293a44ebc2b46a49c64a739c3ad | |
| parent | ac630f12c9d80c9387d44f3f1a1b22db5b5b89da (diff) | |
Excluding explicitly coinductive types in Scheme Equality (#5284).
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 3 | ||||
| -rw-r--r-- | toplevel/auto_ind_decl.mli | 1 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 3 |
3 files changed, 7 insertions, 0 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index a527be32ba..ace99b7bbe 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -56,6 +56,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported +exception NoDecidabilityCoInductive let dl = Loc.ghost @@ -301,6 +302,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 b6c66a1e84..bdfe6e3fa7 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -24,6 +24,7 @@ exception InductiveWithSort exception ParameterWithoutEquality of constant 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 0e59f1aa98..a430d0ded2 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -188,6 +188,9 @@ let try_declare_scheme what f internal names kn = | 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 Errors.noncritical e -> alarm what internal (str "Unexpected error during scheme creation: " ++ Errors.print e) |