From 3264fdaa71b2327a992286a08df0dfbcf78ea4fe Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 7 Jul 2015 17:31:04 +0200
Subject: Checker: Fix bug #4282

Adapt to new [projection] abstract type comprising a constant and
a boolean.
---
 checker/cic.mli         |  2 +-
 checker/closure.ml      | 11 ++++++-----
 checker/closure.mli     |  4 ++--
 checker/declarations.ml | 13 +++++++------
 checker/environ.ml      |  4 ++--
 checker/environ.mli     |  2 +-
 checker/print.ml        |  2 +-
 checker/reduction.ml    |  6 ++++--
 checker/term.ml         |  2 +-
 checker/values.ml       | 11 +++++++----
 10 files changed, 32 insertions(+), 25 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index e875e40f0a..d75af76547 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -102,7 +102,7 @@ type constr =
   | Case      of case_info * constr * constr * constr array
   | Fix       of constr pfixpoint
   | CoFix     of constr pcofixpoint
-  | Proj      of constant * constr
+  | Proj      of projection * constr
 
 type existential = constr pexistential
 type rec_declaration = constr prec_declaration
diff --git a/checker/closure.ml b/checker/closure.ml
index 356b683fa8..c6cc2185d3 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -276,7 +276,7 @@ and fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -308,7 +308,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -678,8 +678,9 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let (depth, args, s) = strip_update_shift_app m s in
       (** Try to drop the params, might fail on partially applied constructors. *)
       let argss = try_drop_parameters depth pars args in
-      let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-					 term = FProj (p, right) }) projs in
+	let hstack =
+	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
+			     term = FProj (Projection.make p false, right) }) projs in
 	argss, [Zapp hstack]	
     | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
@@ -738,7 +739,7 @@ let rec knh info m stk =
     | FCast(t,_,_) -> knh info t stk
 
     | FProj (p,c) ->
-      if red_set info.i_flags (fCONST p) then
+      if red_set info.i_flags (fCONST (Projection.constant p)) then
         (let pb = lookup_projection p (info.i_env) in
 	   knh info c (Zproj (pb.proj_npars, pb.proj_arg, p)
 		       :: zupdate m stk))
diff --git a/checker/closure.mli b/checker/closure.mli
index e6b39250d6..376e9fef7d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -95,7 +95,7 @@ type fterm =
   | FInd of pinductive
   | FConstruct of pconstructor
   | FApp of fconstr * fconstr array
-  | FProj of constant * fconstr
+  | FProj of projection * fconstr
   | FFix of fixpoint * fconstr subs
   | FCoFix of cofixpoint * fconstr subs
   | FCase of case_info * fconstr * fconstr * fconstr array
@@ -117,7 +117,7 @@ type stack_member =
   | Zapp of fconstr array
   | Zcase of case_info * fconstr * fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
+  | Zproj of int * int * projection
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 8d913475f9..36e6a7caba 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -206,14 +206,15 @@ let rec map_kn f f' c =
   let func = map_kn f f' in
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
-      | Proj (kn,t) -> 
-          let kn' = 
-	    try fst (f' kn Univ.Instance.empty)
-	    with No_subst -> kn 
+      | Proj (p,t) -> 
+          let p' = 
+	    Projection.map (fun kn ->
+			    try fst (f' kn Univ.Instance.empty)
+			    with No_subst -> kn) p
 	  in
 	  let t' = func t in
-	    if kn' == kn && t' == t then c
-	    else Proj (kn', t')
+	    if p' == p && t' == t then c
+	    else Proj (p', t')
       | Ind ((kn,i),u) ->
 	  let kn' = f kn in
 	  if kn'==kn then c else Ind ((kn',i),u)
diff --git a/checker/environ.ml b/checker/environ.ml
index 710ebc7127..c0f366000a 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -147,8 +147,8 @@ let evaluable_constant cst env =
 let is_projection cst env = 
   not (Option.is_empty (lookup_constant cst env).const_proj)
 
-let lookup_projection cst env =
-  match (lookup_constant cst env).const_proj with 
+let lookup_projection p env =
+  match (lookup_constant (Projection.constant p) env).const_proj with 
   | Some pb -> pb
   | None -> anomaly ("lookup_projection: constant is not a projection")
 
diff --git a/checker/environ.mli b/checker/environ.mli
index d3448b127f..22fe7d8f17 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -51,7 +51,7 @@ val constant_value : env -> constant puniverses -> constr
 val evaluable_constant : constant -> env -> bool
 
 val is_projection : constant -> env -> bool
-val lookup_projection : constant -> env -> projection_body
+val lookup_projection : projection -> env -> projection_body
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/print.ml b/checker/print.ml
index 1cc48ff774..7624fd3257 100644
--- a/checker/print.ml
+++ b/checker/print.ml
@@ -100,7 +100,7 @@ let print_pure_constr csr =
         done
       in print_string"{"; print_fix (); print_string"}"
   | Proj (p, c) ->
-    print_string "Proj("; sp_con_display p; print_string ","; 
+    print_string "Proj("; sp_con_display (Projection.constant p); print_string ","; 
     box_display c; print_string ")"
 
   and box_display c = open_hovbox 1; term_display c; close_box()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 28fdb130e8..58f0f894ff 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -52,7 +52,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.constant * lift
+  | Zlproj of Names.projection * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -137,7 +137,9 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-	      if not (Names.eq_con_chk c1 c2) then 
+	       if not (Names.eq_con_chk
+		       (Names.Projection.constant c1)
+		       (Names.Projection.constant c2)) then 
 		raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
diff --git a/checker/term.ml b/checker/term.ml
index 93540276b7..430be49519 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -392,7 +392,7 @@ let compare_constr f t1 t2 =
       Array.equal f tl1 tl2 && Array.equal f bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
       Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | Proj (p1,c1), Proj(p2,c2) -> eq_con_chk p1 p2 && f c1 c2
+  | Proj (p1,c1), Proj(p2,c2) -> Projection.equal p1 p2 && f c1 c2
   | _ -> false
 
 let rec eq_constr m n =
diff --git a/checker/values.ml b/checker/values.ml
index b2d74821d4..46b66adc4a 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli
+MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
 
 *)
 
@@ -126,6 +126,7 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
+let v_proj = v_tuple "projection" [|v_cst; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -145,7 +146,7 @@ let rec v_constr =
     [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
-    [|v_cst;v_constr|] (* Proj *)
+    [|v_proj;v_constr|] (* Proj *)
   |])
 
 and v_prec = Tuple ("prec_declaration",
@@ -205,8 +206,10 @@ let v_cst_def =
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
 let v_projbody =
-  v_tuple "projection_body" [|v_cst;Int;Int;v_constr;v_tuple "proj_eta" [|v_constr;v_constr|];
-			      v_constr|]
+  v_tuple "projection_body"
+	  [|v_cst;Int;Int;v_constr;
+	    v_tuple "proj_eta" [|v_constr;v_constr|];
+	    v_constr|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
-- 
cgit v1.2.3


From c71cff0328fa0ee640f35337278f344e0d00698a Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Jul 2015 12:44:59 +0200
Subject: Checker: Report bugfixes from kernel/inductive.ml

Wrong handling of mind_params_ctxt...
---
 checker/inductive.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 59d1a645a5..1c8f570df9 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,12 +104,14 @@ let instantiate_params full t u args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
-    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+  let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
+    subst_instance_context u ar
 
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) u params mib.mind_params_ctxt)
+
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+    instantiate_params true inst_ind u params
+		       (subst_instance_context u mib.mind_params_ctxt)
 
 (************************************************************************)
 (************************************************************************)
-- 
cgit v1.2.3


From 3a6b08286ac78c674d6d3e3073b38de26a610fdc Mon Sep 17 00:00:00 2001
From: mlasson
Date: Mon, 22 Jun 2015 21:14:20 +0200
Subject: Template polymorphism: A bug-fix for Bug #4258

Reviewed by M. Sozeau
This commit fixes template polymorphism and makes it more precise,
applying to non-linear uses of the same universe in parameters of
template-polymorphic inductives. See bug report and
https://github.com/coq/coq/pull/69 for full details.

I also removed some deadcode in checker/inductive.ml.
I do not know if it is also necessary to fix checker/indtypes.ml.
---
 checker/inductive.ml | 83 ++++++++++++++++++++++++++++------------------------
 1 file changed, 45 insertions(+), 38 deletions(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 1c8f570df9..5d31649737 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -144,53 +144,60 @@ let sort_as_univ = function
 | Prop Null -> Univ.type0m_univ
 | Prop Pos -> Univ.type0_univ
 
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
-
-let actualize_decl_level env lev t =
-  let sign,s = dest_arity env t in
-  mkArity (sign,lev)
-
-let polymorphism_on_non_applied_parameters = false
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env a)) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign,Univ.LMap.empty
-  | [], _, _ ->
-      assert false
-
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_ as t)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* a useless extra constraint *)
+        let s = sort_as_univ (snd (dest_arity env a)) in
+        make (cons_subst u s subst) (sign, exp, args)
+    | (na,None,t as d)::sign, Some u::exp, [] ->
+        (* No more argument here: we add the remaining universes to the *)
+        (* substitution (when [u] is distinct from all other universes in the *)
+        (* template, it is identity substitution  otherwise (ie. when u is *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  in
+  make Univ.LMap.empty
 
 exception SingletonInductiveBecomesProp of Id.t
 
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
-  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let subst = make_subst env (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
-- 
cgit v1.2.3


From 2c59d19ad207a6bf193e9f0c9d73258b3133d484 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 9 Jul 2015 16:58:06 +0200
Subject: Kernel/Checker: Cleanup fixes of substitutions due to let-ins.

Avoid undeeded large substitutions, and add test-suite file for
fixed bug 4283 in closed/
---
 checker/inductive.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 5d31649737..e3d8dd2060 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -104,14 +104,11 @@ let instantiate_params full t u args sign =
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
   let t = mkArity (sign,dummy) in
-  let ar = fst (destArity (instantiate_params true t u params mib.mind_params_ctxt)) in
-    subst_instance_context u ar
-
+    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
   let inst_ind = constructor_instantiate mind u mib t in
-    instantiate_params true inst_ind u params
-		       (subst_instance_context u mib.mind_params_ctxt)
+    instantiate_params true inst_ind u params mib.mind_params_ctxt
 
 (************************************************************************)
 (************************************************************************)
-- 
cgit v1.2.3


From 9c732a5c878bac2592cb397aca3d17cfefdcd023 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 01:13:59 +0200
Subject: Option -type-in-type: added support in checker and making it
 contaminating in vo files (this was not done yet in 24d0027f0 and
 090fffa57b).

Reused field "engagement" to carry information about both
impredicativity of set and type in type.

For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
---
 checker/check_stat.ml  | 18 ++++++++++++------
 checker/checker.ml     | 14 +++++++++-----
 checker/cic.mli        |  7 +++++--
 checker/environ.ml     | 25 +++++++++++++++++--------
 checker/environ.mli    |  4 ++--
 checker/indtypes.ml    |  4 ++--
 checker/reduction.ml   |  7 ++++---
 checker/safe_typing.ml | 22 +++++++++++++++-------
 checker/typeops.ml     |  2 +-
 checker/values.ml      |  6 ++++--
 10 files changed, 71 insertions(+), 38 deletions(-)

(limited to 'checker')

diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 05a2a1b992..d041f1b7e1 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -23,11 +23,17 @@ let print_memory_stat () =
 
 let output_context = ref false
 
-let pr_engt = function
-    Some ImpredicativeSet ->
-      str "Theory: Set is impredicative"
-  | None ->
-      str "Theory: Set is predicative"
+let pr_engagement (impr_set,type_in_type) =
+  begin
+    match impr_set with
+    | ImpredicativeSet -> str "Theory: Set is impredicative"
+    | PredicativeSet -> str "Theory: Set is predicative"
+  end ++
+  begin
+    match type_in_type with
+    | StratifiedType -> str "Theory: Stratified type hierarchy"
+    | TypeInType -> str "Theory: Type is of type Type"
+  end
 
 let cst_filter f csts =
   Cmap_env.fold
@@ -54,7 +60,7 @@ let print_context env =
     ppnl(hov 0
       (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
       str"===============" ++ fnl() ++ fnl() ++
-      str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
+      str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++
       str "* " ++ hov 0 (pr_ax csts) ++
       fnl())); pp_flush()
   end
diff --git a/checker/checker.ml b/checker/checker.ml
index 0f7ed8df51..d5d9b9e3b8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -138,10 +138,11 @@ let init_load_path () =
 
 let set_debug () = Flags.debug := true
 
-let engagement = ref None
-let set_engagement c = engagement := Some c
-let engage () =
-  match !engagement with Some c -> Safe_typing.set_engagement c | None -> ()
+let impredicative_set = ref Cic.PredicativeSet
+let set_impredicative_set () = impredicative_set := Cic.ImpredicativeSet
+let type_in_type = ref Cic.StratifiedType
+let set_type_in_type () = type_in_type := Cic.TypeInType
+let engage () = Safe_typing.set_engagement (!impredicative_set,!type_in_type)
 
 
 let admit_list = ref ([] : section_path list)
@@ -194,6 +195,7 @@ let print_usage_channel co command =
 \n  -silent                disable trace of constants being checked\
 \n\
 \n  -impredicative-set     set sort Set impredicative\
+\n  -type-in-type          collapse type hierarchy\
 \n\
 \n  -h, --help             print this list of options\
 \n"
@@ -319,7 +321,9 @@ let parse_args argv =
   let rec parse = function
     | [] -> ()
     | "-impredicative-set" :: rem ->
-      set_engagement Cic.ImpredicativeSet; parse rem
+      set_impredicative_set (); parse rem
+    | "-type-in-type" :: rem ->
+      set_type_in_type (); parse rem
 
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
diff --git a/checker/cic.mli b/checker/cic.mli
index d75af76547..881d3ca797 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -165,7 +165,10 @@ type action
 
 (** Engagements *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -407,7 +410,7 @@ type compiled_library = {
   comp_name : compilation_unit_name;
   comp_mod : module_body;
   comp_deps : library_deps;
-  comp_enga : engagement option;
+  comp_enga : engagement;
   comp_natsymbs : nativecode_symb_array
 }
 
diff --git a/checker/environ.ml b/checker/environ.ml
index c0f366000a..6dbc44d6b8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -14,7 +14,7 @@ type globals = {
 
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option
+  env_engagement : engagement
 }
 
 type env = {
@@ -33,19 +33,28 @@ let empty_env = {
   env_rel_context = [];
   env_stratification =
   { env_universes = Univ.initial_universes;
-    env_engagement = None};
+    env_engagement = (PredicativeSet,StratifiedType)};
   env_imports = MPmap.empty }
 
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let rel_context env = env.env_rel_context
 
-let set_engagement c env =
-  match env.env_stratification.env_engagement with
-    | Some c' -> if c=c' then env else error "Incompatible engagement"
-    | None ->
-        { env with env_stratification =
-          { env.env_stratification with env_engagement = Some c } }
+let set_engagement (impr_set,type_in_type as c) env =
+  let expected_impr_set,expected_type_in_type =
+    env.env_stratification.env_engagement in
+  begin
+    match impr_set,expected_impr_set with
+    | PredicativeSet, ImpredicativeSet -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  begin
+    match type_in_type,expected_type_in_type with
+    | StratifiedType, TypeInType -> error "Incompatible engagement"
+    | _ -> ()
+  end;
+  { env with env_stratification =
+      { env.env_stratification with env_engagement = c } }
 
 (* Digests *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 22fe7d8f17..f3b2dd839a 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -11,7 +11,7 @@ type globals = {
   env_modtypes : module_type_body MPmap.t}
 type stratification = {
   env_universes : Univ.universes;
-  env_engagement : engagement option;
+  env_engagement : engagement;
 }
 type env = {
   env_globals : globals;
@@ -22,7 +22,7 @@ type env = {
 val empty_env : env
 
 (* Engagement *)
-val engagement : env -> Cic.engagement option
+val engagement : env -> Cic.engagement
 val set_engagement : Cic.engagement -> env -> env
 
 (* Digests *)
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 050c33e603..e1a6bc7c1d 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -176,7 +176,7 @@ let typecheck_arity env params inds =
 (* Allowed eliminations *)
 
 let check_predicativity env s small level =
-  match s, engagement env with
+  match s, fst (engagement env) with
       Type u, _ ->
         (* let u' = fresh_local_univ () in *)
         (* let cst = *)
@@ -184,7 +184,7 @@ let check_predicativity env s small level =
         (*     (universes env) in *)
         if not (Univ.check_leq (universes env) level u) then
           failwith "impredicative Type inductive type"
-    | Prop Pos, Some ImpredicativeSet -> ()
+    | Prop Pos, ImpredicativeSet -> ()
     | Prop Pos, _ ->
         if not small then failwith "impredicative Set inductive type"
     | Prop Null,_ -> ()
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 58f0f894ff..8ddeea2a20 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -158,7 +158,7 @@ type conv_pb =
   | CONV
   | CUMUL
 
-let sort_cmp univ pb s0 s1 =
+let sort_cmp env univ pb s0 s1 =
   match (s0,s1) with
     | (Prop c1, Prop c2) when pb = CUMUL -> if c1 = Pos && c2 = Null then raise NotConvertible
     | (Prop c1, Prop c2) -> if c1 <> c2 then raise NotConvertible
@@ -167,7 +167,8 @@ let sort_cmp univ pb s0 s1 =
             CUMUL -> ()
           | _ -> raise NotConvertible)
     | (Type u1, Type u2) ->
-        if not
+        if snd (engagement env) == StratifiedType
+          && not
 	  (match pb with
             | CONV -> Univ.check_eq univ u1 u2
 	    | CUMUL -> Univ.check_leq univ u1 u2)
@@ -261,7 +262,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 	(match a1, a2 with
 	   | (Sort s1, Sort s2) ->
 	       assert (is_empty_stack v1 && is_empty_stack v2);
-	       sort_cmp univ cv_pb s1 s2
+	       sort_cmp (infos_env infos) univ cv_pb s1 s2
 	   | (Meta n, Meta m) ->
                if n=m
 	       then convert_stacks univ infos lft1 lft2 v1 v2
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 810d6e0b65..dd94823135 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -32,13 +32,21 @@ let full_add_module dp mb univs digest =
   let env = Modops.add_module mb env in
   genv := add_digest env dp digest
 
-(* Check that the engagement expected by a library matches the initial one *)
-let check_engagement env c =
-  match engagement env, c with
-    | Some ImpredicativeSet, Some ImpredicativeSet -> ()
-    | _, None -> ()
-    | _, Some ImpredicativeSet ->
-        error "Needs option -impredicative-set"
+(* Check that the engagement expected by a library extends the initial one *)
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (* Libraries = Compiled modules *)
 
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 9bc4b269b8..21819992a9 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -128,7 +128,7 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        if engagement env = Some ImpredicativeSet then
+        if fst (engagement env) = ImpredicativeSet then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
         else
diff --git a/checker/values.ml b/checker/values.ml
index 46b66adc4a..e82ba10327 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -193,7 +193,9 @@ let v_lazy_constr =
 
 (** kernel/declarations *)
 
-let v_engagement = v_enum "eng" 1
+let v_impredicative_set = v_enum "impr-set" 2
+let v_type_in_type = v_enum "type-in-type" 2
+let v_engagement = v_tuple "eng" [|v_impredicative_set; v_type_in_type|]
 
 let v_pol_arity =
   v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
@@ -315,7 +317,7 @@ and v_modtype =
 let v_vodigest = Sum ("module_impl",0, [| [|String|]; [|String;String|] |])
 let v_deps = Array (v_tuple "dep" [|v_dp;v_vodigest|])
 let v_compiled_lib =
-  v_tuple "compiled" [|v_dp;v_module;v_deps;Opt v_engagement;Any|]
+  v_tuple "compiled" [|v_dp;v_module;v_deps;v_engagement;Any|]
 
 (** Library objects *)
 
-- 
cgit v1.2.3


From 1391955c6635da17b4fb2d7c7b5cec799685e99d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 10 Jul 2015 10:26:57 +0200
Subject: Unused variables reported by OCaml.

---
 checker/inductive.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index e3d8dd2060..00d3bc8e14 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -161,7 +161,7 @@ let remember_subst u subst =
 (* Propagate the new levels in the signature *)
 let rec make_subst env =
   let rec make subst = function
-    | (_,Some _,_ as t)::sign, exp, args ->
+    | (_,Some _,_)::sign, exp, args ->
         make subst (sign, exp, args)
     | d::sign, None::exp, args ->
         let args = match args with _::args -> args | [] -> [] in
@@ -174,7 +174,7 @@ let rec make_subst env =
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env a)) in
         make (cons_subst u s subst) (sign, exp, args)
-    | (na,None,t as d)::sign, Some u::exp, [] ->
+    | (na,None,t)::sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
         (* template, it is identity substitution  otherwise (ie. when u is *)
-- 
cgit v1.2.3


From b3f8288b2243efe59d3358ad4001dd78d62308b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 11 Jul 2015 23:59:32 +0200
Subject: Updating checksum in checker (9c732a5cc continued).

Calling md5sum test earlier, at the time coqchk is built, rather than
at testing time, hopefully moving it closer to what it is supposed to
occur.
---
 checker/values.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/values.ml b/checker/values.ml
index e82ba10327..45220bd051 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 cabb12868c5ab7a51dbc6dc2ae8c0894 checker/cic.mli
+MD5 8b7e75b4b94a2d8506a62508e0374c0a checker/cic.mli
 
 *)
 
-- 
cgit v1.2.3


From c57c7edbe517851c7309112f6eb5d8297f03e000 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 15 Jul 2015 17:36:58 +0200
Subject: Univs/Inductive: fix typechecking of cases

I was trying to be a bit too clever with not substituting the universe
instance everywhere: the constructor type/inductive arity has to be
instantiated before instantiate_params runs, which became true only
for constructor types since my last commit.
---
 checker/inductive.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'checker')

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 00d3bc8e14..21b80f323e 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -103,7 +103,7 @@ let instantiate_params full t u args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = Prop Null in
-  let t = mkArity (sign,dummy) in
+  let t = mkArity (subst_instance_context u sign,dummy) in
     fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
 let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
-- 
cgit v1.2.3