diff options
| -rw-r--r-- | Makefile.build | 6 | ||||
| -rwxr-xr-x | configure | 7 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 3 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 1 | ||||
| -rw-r--r-- | tactics/inv.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/1963.v | 19 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
7 files changed, 37 insertions, 7 deletions
diff --git a/Makefile.build b/Makefile.build index 908b61062..bada7f20e 100644 --- a/Makefile.build +++ b/Makefile.build @@ -750,16 +750,16 @@ toplevel/mltop.cmx: toplevel/mltop.optml | toplevel/mltop.ml4.ml.d toplevel/mlto $(SHOW)'OCAMLOPT $<' $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -c -impl $< -o $@ -## This works depency-wise because the dependencies of the +## This works dependency-wise because the dependencies of the ## .{opt,byte}ml files are those we deduce from the .ml4 file. ## In other words, the Byte-only code doesn't import a new module. -toplevel/mltop.byteml: toplevel/mltop.ml4 # no camlp4deps here +toplevel/mltop.byteml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ -DByte -DHasDynlink -impl $< > $@ \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) -toplevel/mltop.optml: toplevel/mltop.ml4 # no camlp4deps here +toplevel/mltop.optml: toplevel/mltop.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' $(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` \ $(NATDYNLINKDEF) -impl $< > $@ \ @@ -445,7 +445,12 @@ fi # Native dynlink if [ "$natdynlink" = "yes" -a -f `"$CAMLC" -where`/dynlink.cmxa ]; then - HASNATDYNLINK=true + case `uname -s`,`uname -r`,$CAMLVERSION in + Darwin,9.*,3.11.0) # ocaml 3.11.0 dynlink on MacOS 10.5 is buggy + HASNATDYNLINK=false;; + *) + HASNATDYNLINK=true;; + esac else HASNATDYNLINK=false fi diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 3452be55c..4aac096fc 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -46,6 +46,7 @@ type inductive_error = | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry + | LargeNonPropInductiveNotInType exception InductiveError of inductive_error @@ -269,7 +270,7 @@ let typecheck_inductive env mie = | Prop Pos when engagement env <> Some ImpredicativeSet -> (* Predicative set: check that the content is indeed predicative *) if not (is_type0m_univ lev) & not (is_type0_univ lev) then - error "Large non-propositional inductive types must be in Type."; + raise (InductiveError LargeNonPropInductiveNotInType); Inl (info,full_arity,s), cst | Prop _ -> Inl (info,full_arity,s), cst in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a583bcb1..0cbe15034 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -33,6 +33,7 @@ type inductive_error = | SameNamesOverlap of identifier list | NotAnArity of identifier | BadEntry + | LargeNonPropInductiveNotInType exception InductiveError of inductive_error diff --git a/tactics/inv.ml b/tactics/inv.ml index 46ce6e20b..ca98cbc6f 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -109,8 +109,8 @@ let make_inv_predicate env sigma indf realargs id status concl = match dflt_concl with | Some concl -> concl (*assumed it's some [x1..xn,H:I(x1..xn)]C*) | None -> - let sort = get_sort_of env sigma concl in - let p = make_arity env true indf sort in + let sort = get_sort_family_of env sigma concl in + let p = make_arity env true indf (new_sort_in_family sort) in Unification.abstract_list_all env (Evd.create_evar_defs sigma) p concl (realargs@[mkVar id]) in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/shouldsucceed/1963.v new file mode 100644 index 000000000..11e2ee44d --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1963.v @@ -0,0 +1,19 @@ +(* Check that "dependent inversion" behaves correctly w.r.t to universes *) + +Require Import Eqdep. + +Set Implicit Arguments. + +Inductive illist(A:Type) : nat -> Type := + illistn : illist A 0 +| illistc : forall n:nat, A -> illist A n -> illist A (S n). + +Inductive isig (A:Type)(P:A -> Type) : Type := + iexists : forall x : A, P x -> isig P. + +Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n -> + isig (fun t => isig (fun ts => + eq_dep nat (fun n => illist A n) n' ts' (S n) (illistc t ts))). +Proof. +intros. +dependent inversion ts'. diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 52581a15d..42fc6d0fc 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -655,6 +655,9 @@ let error_not_an_arity id = let error_bad_entry () = str "Bad inductive definition." +let error_large_non_prop_inductive_not_in_type () = + str "Large non-propositional inductive types must be in Type." + (* Recursion schemes errors *) let error_not_allowed_case_analysis isrec kind i = @@ -685,6 +688,7 @@ let explain_inductive_error = function | SameNamesOverlap idl -> error_same_names_overlap idl | NotAnArity id -> error_not_an_arity id | BadEntry -> error_bad_entry () + | LargeNonPropInductiveNotInType -> error_large_non_prop_inductive_not_in_type () (* Recursion schemes errors *) |