From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 checker/indtypes.ml | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

(limited to 'checker/indtypes.ml')

diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 277fed30..1e773df6 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 10296 2007-11-07 11:02:42Z barras $ *)
-
 open Util
 open Names
 open Univ
@@ -178,7 +176,7 @@ let check_predicativity env s small level =
       Type u, _ ->
         let u' = fresh_local_univ () in
         let cst =
-          merge_constraints (enforce_geq u' u Constraint.empty)
+          merge_constraints (enforce_geq u' u empty_constraint)
             (universes env) in
         if not (check_geq cst u' level) then
           failwith "impredicative Type inductive type"
@@ -394,7 +392,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c =
 
 (* The recursive function that checks positivity and builds the list
    of recursive arguments *)
-let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
+let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc =
   let lparams = rel_context_length hyps in
   (* check the inductive types occur positively in [c] *)
   let rec check_pos (env, n, ntypes, ra_env as ienv) c =
@@ -496,7 +494,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp i indlc =
           with IllFormedInd err ->
             explain_ind_err (ntypes-i) env lparams c err)
       indlc
-  in mk_paths (Mrec i) irecargs
+  in mk_paths (Mrec ind) irecargs
 
 let check_subtree (t1:'a) (t2:'a) =
   if not (Rtree.compare_rtree (fun t1 t2 ->
@@ -507,16 +505,17 @@ let check_subtree (t1:'a) (t2:'a) =
     failwith "bad recursive trees"
 (* if t1=t2 then () else msg_warning (str"TODO: check recursive positions")*)
 
-let check_positivity env_ar params nrecp inds =
+let check_positivity env_ar mind params nrecp inds =
   let ntypes = Array.length inds in
-  let rc = Array.mapi (fun j t -> (Mrec j,t)) (Rtree.mk_rec_calls ntypes) in
+  let rc =
+    Array.mapi (fun j t -> (Mrec(mind,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = List.rev (Array.to_list rc) in
   let lparams = rel_context_length params in
   let check_one i mip =
     let ra_env =
       list_tabulate (fun _ -> (Norec,mk_norec)) lparams @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-      check_positivity_one ienv params nrecp i mip.mind_nf_lc
+      check_positivity_one ienv params nrecp (mind,i) mip.mind_nf_lc
   in
   let irecargs = Array.mapi check_one inds in
   let wfp = Rtree.mk_rec irecargs in
@@ -549,7 +548,7 @@ let check_inductive env kn mib =
   (*  - check constructor types *)
   Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets;
   (* check mind_nparams_rec: positivity condition *)
-  check_positivity env_ar params mib.mind_nparams_rec mib.mind_packets;
+  check_positivity env_ar kn params mib.mind_nparams_rec mib.mind_packets;
   (* check mind_equiv... *)
   (* Now we can add the inductive *)
   add_mind kn mib env
-- 
cgit v1.2.3