*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7899 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 19 insertions, 8 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 83928b6cca..643dd4da2a 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -20,10 +20,14 @@ open Reduction
 open Typeops
 open Entries
 
-(* [check_constructors_names id s cl] checks that all the constructors names
-   appearing in [l] are not present in the set [s], and returns the new set
-   of names. The name [id] is the name of the current inductive type, used
-   when reporting the error. *)
+(* Same as noccur_between but may perform reductions.
+   Could be refined more...  *)
+let weaker_noccur_between env x nvars t =
+  if noccur_between x nvars t then Some t
+  else
+   let t' = whd_betadeltaiota env t in
+   if noccur_between x nvars t' then Some t'
+   else None
 
 (************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
@@ -42,6 +46,11 @@ type inductive_error =
 
 exception InductiveError of inductive_error
 
+(* [check_constructors_names id s cl] checks that all the constructors names
+   appearing in [l] are not present in the set [s], and returns the new set
+   of names. The name [id] is the name of the current inductive type, used
+   when reporting the error. *)
+
 let check_constructors_names id =
   let rec check idset = function
     | [] -> idset
@@ -357,10 +366,10 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps i indlc =
     match kind_of_term x with
       | Prod (na,b,d) ->
 	  assert (largs = []);
-	  let b = whd_betadeltaiota env b in
-          if not (noccur_between n ntypes b) then
-	    raise (IllFormedInd (LocalNonPos n));
-	  check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d
+          (match weaker_noccur_between env n ntypes b with
+              None -> raise (IllFormedInd (LocalNonPos n));
+            | Some b ->
+	        check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
       | Rel k ->
            (try let (ra,rarg) = List.nth ra_env (k-1) in 
 		let nmr1 =
diff --git a/library/global.mli b/library/global.mli
index a6ed6f4114..5798824985 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -35,6 +35,8 @@ val universes : unit -> universes
 val named_context_val : unit -> Environ.named_context_val
 val named_context : unit -> Sign.named_context
 
+val env_is_empty : unit -> bool
+
 (*s Extending env with variables and local definitions *)
 val push_named_assum : (identifier * types) -> Univ.constraints
 val push_named_def   : (identifier * constr * types option) -> Univ.constraints