- 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

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 *)