diff options
| author | Hugo Herbelin | 2018-09-19 22:47:36 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 13:28:36 +0200 |
| commit | 82a3fb5d5c0d0c5660effec59f3800ee5e8a125d (patch) | |
| tree | daf3db3f650308c37d65b285788e4e034f1d04ad | |
| parent | 0e225553a2ee1c39e0f070edb6528d109dd878ac (diff) | |
Fixing #4859 (anomaly with Scheme called on inductive type with indices).
We raise a normal error instead of an anomaly.
| -rw-r--r-- | test-suite/bugs/closed/4859.v | 7 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 6 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.mli | 1 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 3 |
4 files changed, 17 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4859.v b/test-suite/bugs/closed/4859.v new file mode 100644 index 0000000000..7be0bedcfc --- /dev/null +++ b/test-suite/bugs/closed/4859.v @@ -0,0 +1,7 @@ +(* Not supported but check at least that it does not raise an anomaly *) + +Inductive Fin{n : nat} : Set := +| F1{i : nat}{e : n = S i} +| FS{i : nat}(f : @ Fin i){e : n = S i}. + +Fail Scheme Equality for Fin. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 25ec1a68b4..ca1d36cb69 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -60,6 +60,7 @@ exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive exception ConstructorWithNonParametricInductiveType of inductive +exception DecidabilityIndicesNotSupported let constr_of_global g = lazy (UnivGen.constr_of_global g) @@ -121,6 +122,10 @@ let check_bool_is_defined () = try let _ = Global.type_of_global_in_context (Global.env ()) Coqlib.glob_bool in () with e when CErrors.noncritical e -> raise (UndefinedCst "bool") +let check_no_indices mib = + if Array.exists (fun mip -> mip.mind_nrealargs <> 0) mib.mind_packets then + raise DecidabilityIndicesNotSupported + let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined") let build_beq_scheme mode kn = @@ -134,6 +139,7 @@ let build_beq_scheme mode kn = (* number of params in the type *) let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in + check_no_indices mib; (* params context divided *) let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in diff --git a/vernac/auto_ind_decl.mli b/vernac/auto_ind_decl.mli index 8ecc09b7d1..647ff3d8d6 100644 --- a/vernac/auto_ind_decl.mli +++ b/vernac/auto_ind_decl.mli @@ -28,6 +28,7 @@ exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive exception ConstructorWithNonParametricInductiveType of inductive +exception DecidabilityIndicesNotSupported val beq_scheme_kind : mutual scheme_kind val build_beq_scheme : mutual_scheme_object_function diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 4c41ea657a..0a74a8cc4a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -177,6 +177,9 @@ let try_declare_scheme what f internal names kn = | NoDecidabilityCoInductive -> alarm what internal (str "Scheme Equality is only for inductive types.") + | DecidabilityIndicesNotSupported -> + alarm what internal + (str "Inductive types with annotations not supported.") | ConstructorWithNonParametricInductiveType ind -> alarm what internal (strbrk "Unsupported constructor with an argument whose type is a non-parametric inductive type." ++ |