aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-11 20:11:18 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-01-11 20:11:18 +0000
commit4d30972530c4ea6792f0c6e47c355a00e3b8c924 (patch)
treeda589bf0ac0de7fc6f7f29d385b62e2e881c55ee
parent99477c6fb60caf8d780d46aefc763d5e594331a0 (diff)
- Deactivation of dynamic loading on Mac OS 10.5 (see bug #2024).
- Added dependency of mltop.ml4 into config/Makefile (see bug #2023). - Fixed bug #1963 (dependent inversion building a universe-ill-formed conversion problem). - Incidentally, moved "Large non-propositional inductive ..." error message to standard himsg.ml error displayer. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11774 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build6
-rwxr-xr-xconfigure7
-rw-r--r--kernel/indtypes.ml3
-rw-r--r--kernel/indtypes.mli1
-rw-r--r--tactics/inv.ml4
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1963.v19
-rw-r--r--toplevel/himsg.ml4
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 $< > $@ \
diff --git a/configure b/configure
index df2b39551..e1b17a64f 100755
--- a/configure
+++ b/configure
@@ -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 *)