diff options
| -rwxr-xr-x | configure | 2 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 2 | ||||
| -rw-r--r-- | toplevel/errors.ml | 2 |
5 files changed, 5 insertions, 9 deletions
@@ -6,7 +6,7 @@ # ################################## -VERSION=7.00 +VERSION=7.0 VERSIONSI=1.0 DATE="November 2000" diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f10e59c9c..2307a405f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -74,8 +74,7 @@ let mind_check_names mie = declaration, and checks that they are all present (and all the same) for all the given types. *) -let mind_extract_params n c = - let (l,c') = decompose_prod_n_assum n c in (l,c') +let mind_extract_params = decompose_prod_n_assum let mind_check_arities env mie = let check_arity id c = diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index b8ea65f16..be97f5249 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -28,11 +28,6 @@ type inductive_error = | BadInduction of bool * identifier * sorts | NotMutualInScheme -(* [mind_extract_params] extracts the parameters of an inductive - type declaration. *) - -val mind_extract_params : int -> constr -> Sign.rel_context * constr - exception InductiveError of inductive_error (*s The following function does checks on inductive declarations. *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a6934b9dc..925ca9bf0 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -470,7 +470,7 @@ let add_mind sp mie env = (ind'::inds, Constraint.union cst cst')) mie.mind_entry_inds params_arity_list - ([],Constraint.empty) in + ([],cst) in (* Finally, we build the inductive packet and push it to env *) let kind = kind_of_path sp in diff --git a/toplevel/errors.ml b/toplevel/errors.ml index c72f2ddb3..6c76e5e88 100644 --- a/toplevel/errors.ml +++ b/toplevel/errors.ml @@ -55,6 +55,8 @@ let rec explain_exn_default = function hOV 0 [< 'sTR "Anomaly: Invalid argument "; 'sTR (guill s); report () >] | Sys.Break -> hOV 0 [< 'fNL; 'sTR"User Interrupt." >] + | Univ.UniverseInconsistency -> + hOV 0 [< 'sTR "Error: Universe Inconsistency." >] | TypeError(k,ctx,te) -> hOV 0 [< 'sTR "Error:"; 'sPC; Himsg.explain_type_error k ctx te >] | InductiveError e -> |