Providing a -type-in-type option for collapsing the universe hierarchy.

12 files changed, 134 insertions, 104 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 8851ea2b66..14afcc4dbb 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1111,6 +1111,8 @@ let create_clos_infos ?(evars=fun _ -> None) flgs env =
   create (fun _ -> inject) flgs env evars
 let oracle_of_infos infos = Environ.oracle infos.i_cache.i_env
 
+let env_of_infos infos = infos.i_cache.i_env
+
 let infos_with_reds infos reds = 
   { infos with i_flags = reds }
 
diff --git a/kernel/closure.mli b/kernel/closure.mli
index adcf258576..1062d0e61b 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -172,6 +172,8 @@ val create_clos_infos :
   ?evars:(existential->constr option) -> reds -> env -> clos_infos
 val oracle_of_infos : clos_infos -> Conv_oracle.oracle
 
+val env_of_infos : clos_infos -> env
+
 val infos_with_reds : clos_infos -> reds -> clos_infos
 
 (** Reduction function *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2a4f3a9485..aa83864c67 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,6 +46,8 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
+let type_in_type env = env.env_stratification.env_type_in_type
+
 let is_impredicative_set env = 
   match engagement env with
   | Some ImpredicativeSet -> true
@@ -189,6 +191,10 @@ let set_engagement c env = (* Unsafe *)
   { env with env_stratification =
     { env.env_stratification with env_engagement = Some c } }
 
+let set_type_in_type env =
+  { env with env_stratification =
+    { env.env_stratification with env_type_in_type = true } }
+
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 1523f40d1f..7f3fdc536b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,6 +50,8 @@ val named_context_val : env -> named_context_val
 val engagement    : env -> engagement option
 val is_impredicative_set : env -> bool
 
+val type_in_type  : env -> bool
+
 (** is the local context empty *)
 val empty_context : env -> bool
 
@@ -210,6 +212,8 @@ val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
 
+val set_type_in_type : env -> env
+
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 5964ed70ed..c7701a8b1e 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,15 +16,15 @@ open Nativecode
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-let rec conv_val pb lvl v1 v2 cu = 
+let rec conv_val env pb lvl v1 v2 cu = 
   if v1 == v2 then cu
   else
     match kind_of_value v1, kind_of_value v2 with
     | Vaccu k1, Vaccu k2 ->
-	conv_accu pb lvl k1 k2 cu
+	conv_accu env pb lvl k1 k2 cu
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
-	conv_val CONV (lvl+1) (f1 v) (f2 v) cu
+	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
     | Vconst i1, Vconst i2 -> 
 	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vblock b1, Vblock b2 ->
@@ -34,29 +34,29 @@ let rec conv_val pb lvl v1 v2 cu =
 	  raise NotConvertible;
 	let rec aux lvl max b1 b2 i cu =
 	  if Int.equal i max then 
-	    conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu
+	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
 	  else
 	    let cu = 
-	      conv_val CONV lvl (block_field b1 i) (block_field b2 i) cu in
+	      conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
 	    aux lvl max b1 b2 (i+1) cu in
 	aux lvl (n1-1) b1 b2 0 cu
     | Vfun f1, _ -> 
-	conv_val CONV lvl v1 (fun x -> v2 x) cu
+	conv_val env CONV lvl v1 (fun x -> v2 x) cu
     | _, Vfun f2 ->
-	conv_val CONV lvl (fun x -> v1 x) v2 cu
+	conv_val env CONV lvl (fun x -> v1 x) v2 cu
     | _, _ -> raise NotConvertible
 
-and conv_accu pb lvl k1 k2 cu = 
+and conv_accu env pb lvl k1 k2 cu = 
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
   if Int.equal n1 0 then 
-    conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
+    conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
-    let cu = conv_atom pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
-    List.fold_right2 (conv_val CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
+    let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+    List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
 
-and conv_atom pb lvl a1 a2 cu =
+and conv_atom env pb lvl a1 a2 cu =
   if a1 == a2 then cu
   else
     match a1, a2 with
@@ -70,18 +70,18 @@ and conv_atom pb lvl a1 a2 cu =
 	if not (eq_constant c1 c2) then raise NotConvertible;
 	cu
     | Asort s1, Asort s2 -> 
-        check_sort_cmp_universes pb s1 s2 cu; cu
+        check_sort_cmp_universes env pb s1 s2 cu; cu
     | Avar id1, Avar id2 ->
 	if not (Id.equal id1 id2) then raise NotConvertible;
 	cu
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
 	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	let cu = conv_accu CONV lvl ac1 ac2 cu in
+	let cu = conv_accu env CONV lvl ac1 ac2 cu in
 	let tbl = a1.asw_reloc in
 	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val CONV lvl p1 p2 cu 
+	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu 
 	else
-	  let cu = conv_val CONV lvl p1 p2 cu in
+	  let cu = conv_val env CONV lvl p1 p2 cu in
 	  let max = len - 1 in
 	  let rec aux i cu =
 	    let tag,arity = tbl.(i) in
@@ -89,38 +89,38 @@ and conv_atom pb lvl a1 a2 cu =
 	      if Int.equal arity 0 then mk_const tag
 	      else mk_block tag (mk_rels_accu lvl arity) in
 	    let bi1 = bs1 ci and bi2 = bs2 ci in
-	    if Int.equal i max then conv_val CONV (lvl + arity) bi1 bi2 cu
-	    else aux (i+1) (conv_val CONV (lvl + arity) bi1 bi2 cu) in
+	    if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+	    else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
 	  aux 0 cu
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
 	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
 	if f1 == f2 then cu
-	else conv_fix lvl t1 f1 t2 f2 cu
+	else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
 	if not (Int.equal s1 s2) then raise NotConvertible;
 	if f1 == f2 then cu
 	else
 	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
-	  else conv_fix lvl t1 f1 t2 f2 cu 
+	  else conv_fix env lvl t1 f1 t2 f2 cu 
     | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
-	let cu = conv_val CONV lvl d1 d2 cu in
+	let cu = conv_val env CONV lvl d1 d2 cu in
 	let v = mk_rel_accu lvl in
-	conv_val pb (lvl + 1) (d1 v) (d2 v) cu 
+	conv_val env pb (lvl + 1) (d1 v) (d2 v) cu 
     | _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
-and conv_fix lvl t1 f1 t2 f2 cu =
+and conv_fix env lvl t1 f1 t2 f2 cu =
   let len = Array.length f1 in
   let max = len - 1 in
   let fargs = mk_rels_accu lvl len in
   let flvl = lvl + len in
   let rec aux i cu =
-    let cu = conv_val CONV lvl t1.(i) t2.(i) cu in
+    let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
     let fi1 = napply f1.(i) fargs in
     let fi2 = napply f2.(i) fargs in
-    if Int.equal i max then conv_val CONV flvl fi1 fi2 cu 
-    else aux (i+1) (conv_val CONV flvl fi1 fi2 cu) in
+    if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu 
+    else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
   aux 0 cu
 
 let native_conv pb sigma env t1 t2 =
@@ -144,7 +144,7 @@ let native_conv pb sigma env t1 t2 =
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
-        ignore(conv_val pb 0 !rt1 !rt2 (Environ.universes env))
+        ignore(conv_val env pb 0 !rt1 !rt2 (Environ.universes env))
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index ba9f302334..a5221c7794 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,7 +46,8 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option
+  env_engagement : engagement option;
+  env_type_in_type : bool
 }
 
 type val_kind =
@@ -92,7 +93,8 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None };
+    env_engagement = None;
+    env_type_in_type = false};
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge }
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 74a5fb1aed..9561333c8d 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,7 +33,8 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option
+  env_engagement : engagement option;
+  env_type_in_type : bool
 }
 
 type lazy_val
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 31c338dd97..802d2b67b4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -177,7 +177,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
@@ -187,8 +187,8 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
-let sort_cmp_universes pb s0 s1 (u, check) =
-  (check.compare pb s0 s1 u, check)
+let sort_cmp_universes env pb s0 s1 (u, check) =
+  (check.compare env pb s0 s1 u, check)
 
 let convert_instances flex u u' (s, check) =
   (check.compare_instances flex u u' s, check)
@@ -310,7 +310,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   | (Sort s1, Sort s2) ->
 	       if not (is_empty_stack v1 && is_empty_stack v2) then
 		 anomaly (Pp.str "conversion was given ill-typed terms (Sort)");
-	       sort_cmp_universes cv_pb s1 s2 cuniv
+	       sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
 	   | (Meta n, Meta m) ->
                if Int.equal n m
 	       then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
@@ -552,7 +552,7 @@ let check_eq univs u u' =
 let check_leq univs u u' = 
   if not (check_leq univs u u') then raise NotConvertible
 
-let check_sort_cmp_universes pb s0 s1 univs =
+let check_sort_cmp_universes env pb s0 s1 univs =
   match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
@@ -566,13 +566,14 @@ let check_sort_cmp_universes pb s0 s1 univs =
 	| CUMUL -> check_leq univs u0 u
 	| CONV -> check_eq univs u0 u)
     | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) -> 
+    | (Type u1, Type u2) ->
+        if not (type_in_type env) then 
 	(match pb with
 	| CUMUL -> check_leq univs u1 u2
 	| CONV -> check_eq univs u1 u2)
 
-let checked_sort_cmp_universes pb s0 s1 univs =
-  check_sort_cmp_universes pb s0 s1 univs; univs
+let checked_sort_cmp_universes env pb s0 s1 univs =
+  check_sort_cmp_universes env pb s0 s1 univs; univs
 
 let check_convert_instances _flex u u' univs =
   if Univ.Instance.check_eq univs u u' then univs
@@ -593,7 +594,7 @@ let infer_leq (univs, cstrs as cuniv) u u' =
     let cstrs' = Univ.enforce_leq u u' cstrs in
       univs, cstrs'
 
-let infer_cmp_universes pb s0 s1 univs =
+let infer_cmp_universes env pb s0 s1 univs =
   match (s0,s1) with
     | (Prop c1, Prop c2) when is_cumul pb ->
       begin match c1, c2 with
@@ -607,10 +608,12 @@ let infer_cmp_universes pb s0 s1 univs =
 	| CUMUL -> infer_leq univs u0 u
 	| CONV -> infer_eq univs u0 u)
     | (Type u, Prop c) -> raise NotConvertible
-    | (Type u1, Type u2) -> 
+    | (Type u1, Type u2) ->
+        if not (type_in_type env) then
 	(match pb with
 	| CUMUL -> infer_leq univs u1 u2
 	| CONV -> infer_eq univs u1 u2)
+        else univs
 
 let infer_convert_instances flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index cfeafd75cb..f0b1761046 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -38,7 +38,7 @@ type conv_pb = CONV | CUMUL
 
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
-    compare : conv_pb -> sorts -> sorts -> 'a -> 'a;
+    compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: bool (* Instance of a flexible constant? *) -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
@@ -50,7 +50,7 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
 val check_sort_cmp_universes :
-  conv_pb -> sorts -> sorts -> Univ.universes -> unit
+  env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit
 
 (* val sort_cmp : *)
 (*     conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 71a6b7a399..f7464013fd 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -81,7 +81,8 @@ open Declarations
       These fields could be deduced from [revstruct], but they allow faster
       name freshness checks.
  - [univ] and [future_cst] : current and future universe constraints
- - [engagement] : are we Set-impredicative ?
+ - [engagement] : are we Set-impredicative?
+ - [type_in_type] : does the universe hierarchy collapse?
  - [imports] : names and digests of Require'd libraries since big-bang.
       This field will only grow
  - [loads] : list of libraries Require'd inside the current module.
@@ -121,6 +122,7 @@ type safe_environment =
     univ : Univ.constraints;
     future_cst : Univ.constraints Future.computation list;
     engagement : engagement option;
+    type_in_type : bool;
     imports : vodigest DPMap.t;
     loads : (module_path * module_body) list;
     local_retroknowledge : Retroknowledge.action list}
@@ -143,6 +145,7 @@ let empty_environment =
     future_cst = [];
     univ = Univ.Constraint.empty;
     engagement = None;
+    type_in_type = false;
     imports = DPMap.empty;
     loads = [];
     local_retroknowledge = [] }
@@ -179,6 +182,10 @@ let check_engagement env c =
     Errors.error "Needs option -impredicative-set."
   | _ -> ()
 
+let set_type_in_type senv = 
+  { senv with
+    env = Environ.set_type_in_type senv.env;
+    type_in_type = true }
 
 (** {6 Stm machinery } *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 429597f90b..6edea363bf 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -97,9 +97,12 @@ val add_constraints :
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
 
-(** Settin the strongly constructive or classical logical engagement *)
+(** Setting the strongly constructive or classical logical engagement *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 
+(** Collapsing the type hierarchy *)
+val set_type_in_type : safe_transformer0
+
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> module_path safe_transformer
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 0e91c79727..976380ede7 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -44,25 +44,25 @@ let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
 let eq_table_key = Names.eq_table_key eq_constant
 
-let rec conv_val pb k v1 v2 cu =
+let rec conv_val env pb k v1 v2 cu =
   if v1 == v2 then cu
-  else conv_whd pb k (whd_val v1) (whd_val v2) cu
+  else conv_whd env pb k (whd_val v1) (whd_val v2) cu
 
-and conv_whd pb k whd1 whd2 cu =
+and conv_whd env pb k whd1 whd2 cu =
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
+  | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
   | Vprod p1, Vprod p2 ->
-      let cu = conv_val CONV k (dom p1) (dom p2) cu in
-      conv_fun pb k (codom p1) (codom p2) cu
-  | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu
-  | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu
+      let cu = conv_val env CONV k (dom p1) (dom p2) cu in
+      conv_fun env pb k (codom p1) (codom p2) cu
+  | Vfun f1, Vfun f2 -> conv_fun env CONV k f1 f2 cu
+  | Vfix (f1,None), Vfix (f2,None) -> conv_fix env k f1 f2 cu
   | Vfix (f1,Some args1), Vfix(f2,Some args2) ->
       if nargs args1 <> nargs args2 then raise NotConvertible
-      else conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
-  | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu
+      else conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu)
+  | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix env k cf1 cf2 cu
   | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->
       if nargs args1 <> nargs args2 then raise NotConvertible
-      else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
+      else conv_arguments env k args1 args2 (conv_cofix env k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 ->
       if Int.equal i1 i2 then cu else raise NotConvertible
   | Vconstr_block b1, Vconstr_block b2 ->
@@ -70,103 +70,103 @@ and conv_whd pb k whd1 whd2 cu =
       if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
-	  rcu := conv_val CONV k (bfield b1 i) (bfield b2 i) !rcu
+	  rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
 	done;
 	!rcu
       else raise NotConvertible
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
-      conv_atom pb k a1 stk1 a2 stk2 cu
+      conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
-      conv_val CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
+      conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
   | _, Vatom_stk(Aiddef(_,v),stk) ->
-      conv_whd pb k whd1 (force_whd v stk) cu
+      conv_whd env pb k whd1 (force_whd v stk) cu
   | Vatom_stk(Aiddef(_,v),stk), _ ->
-      conv_whd pb k (force_whd v stk) whd2 cu
+      conv_whd env pb k (force_whd v stk) whd2 cu
   | _, _ -> raise NotConvertible
 
-and conv_atom pb k a1 stk1 a2 stk2 cu =
+and conv_atom env pb k a1 stk1 a2 stk2 cu =
   match a1, a2 with
   | Aind (kn1,i1), Aind(kn2,i2) ->
       if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
       then
-	conv_stack k stk1 stk2 cu
+	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 ->
       if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
-	conv_stack k stk1 stk2 cu
+	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
       begin
 	try
 	  if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then
-	    conv_stack k stk1 stk2 cu
+	    conv_stack env k stk1 stk2 cu
 	  else raise NotConvertible
 	with NotConvertible ->
 	  if oracle_order (oracle_of_infos !infos) false ik1 ik2 then
-            conv_whd pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
-          else conv_whd pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+            conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+          else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
       end
   | Aiddef(ik1,v1), _ ->
-      conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
+      conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
-      conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
+      conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
   | _, _ -> raise NotConvertible
 
-and conv_stack k stk1 stk2 cu =
+and conv_stack env k stk1 stk2 cu =
   match stk1, stk2 with
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
-      conv_stack k stk1 stk2 (conv_arguments k args1 args2 cu)
+      conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
   | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
-      conv_stack k stk1 stk2
-	(conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
+      conv_stack env k stk1 stk2
+	(conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
       if check_switch sw1 sw2 then
 	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
-	let rcu = ref (conv_val CONV k vt1 vt2 cu) in
+	let rcu = ref (conv_val env CONV k vt1 vt2 cu) in
 	let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
 	for i = 0 to Array.length b1 - 1 do
 	  rcu :=
-	    conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
+	    conv_val env CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
 	done;
-	conv_stack k stk1 stk2 !rcu
+	conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
   | _, _ -> raise NotConvertible
 
-and conv_fun pb k f1 f2 cu =
+and conv_fun env pb k f1 f2 cu =
   if f1 == f2 then cu
   else
     let arity,b1,b2 = decompose_vfun2 k f1 f2 in
-    conv_val pb (k+arity) b1 b2 cu
+    conv_val env pb (k+arity) b1 b2 cu
 
-and conv_fix k f1 f2 cu =
+and conv_fix env k f1 f2 cu =
   if f1 == f2 then cu
   else
     if check_fix f1 f2 then
       let bf1, tf1 = reduce_fix k f1 in
       let bf2, tf2 = reduce_fix k f2 in
-      let cu = conv_vect (conv_val CONV k) tf1 tf2 cu in
-      conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu
+      let cu = conv_vect (conv_val env CONV k) tf1 tf2 cu in
+      conv_vect (conv_fun env CONV (k + Array.length tf1)) bf1 bf2 cu
     else raise NotConvertible
 
-and conv_cofix k cf1 cf2 cu =
+and conv_cofix env k cf1 cf2 cu =
   if cf1 == cf2 then cu
   else
     if check_cofix cf1 cf2 then
       let bcf1, tcf1 = reduce_cofix k cf1 in
       let bcf2, tcf2 = reduce_cofix k cf2 in
-      let cu = conv_vect (conv_val CONV k) tcf1 tcf2 cu in
-      conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu
+      let cu = conv_vect (conv_val env CONV k) tcf1 tcf2 cu in
+      conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
     else raise NotConvertible
 
-and conv_arguments k args1 args2 cu =
+and conv_arguments env k args1 args2 cu =
   if args1 == args2 then cu
   else
     let n = nargs args1 in
     if Int.equal n (nargs args2) then
       let rcu = ref cu in
       for i = 0 to n - 1 do
-	rcu := conv_val CONV k (arg args1 i) (arg args2 i) !rcu
+	rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
       done;
       !rcu
     else raise NotConvertible
@@ -178,7 +178,7 @@ let rec eq_puniverses f (x,l1) (y,l2) cu =
 and conv_universes l1 l2 cu =
   if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
 
-let rec conv_eq pb t1 t2 cu =
+let rec conv_eq env pb t1 t2 cu =
   if t1 == t2 then cu
   else
     match kind_of_term t1, kind_of_term t2 with
@@ -188,55 +188,55 @@ let rec conv_eq pb t1 t2 cu =
 	if Int.equal m1 m2 then cu else raise NotConvertible
     | Var id1, Var id2 ->
 	if Id.equal id1 id2 then cu else raise NotConvertible
-    | Sort s1, Sort s2 -> check_sort_cmp_universes pb s1 s2 cu; cu
-    | Cast (c1,_,_), _ -> conv_eq pb c1 t2 cu
-    | _, Cast (c2,_,_) -> conv_eq pb t1 c2 cu
+    | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
+    | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu
+    | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu
     | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu
+	conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu)
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu
     | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	conv_eq pb c1 c2 (conv_eq CONV b1 b2 cu)
+	conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu)
     | App (c1,l1), App (c2,l2) ->
-	conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu)
+	conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu)
     | Evar (e1,l1), Evar (e2,l2) ->
-	if Evar.equal e1 e2 then conv_eq_vect l1 l2 cu
+	if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu
 	else raise NotConvertible
     | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
     | Proj (p1,c1), Proj (p2,c2) ->
-	if eq_constant p1 p2 then conv_eq pb c1 c2 cu else raise NotConvertible
+	if eq_constant p1 p2 then conv_eq env pb c1 c2 cu else raise NotConvertible
     | Ind c1, Ind c2 ->
        eq_puniverses eq_ind c1 c2 cu
     | Construct c1, Construct c2 ->
        eq_puniverses eq_constructor c1 c2 cu
     | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	let pcu = conv_eq CONV p1 p2 cu in
-	let ccu = conv_eq CONV c1 c2 pcu in
-	conv_eq_vect bl1 bl2 ccu
+	let pcu = conv_eq env CONV p1 p2 cu in
+	let ccu = conv_eq env CONV c1 c2 pcu in
+	conv_eq_vect env bl1 bl2 ccu
     | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-	if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+	if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
 	else raise NotConvertible
     | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	if Int.equal ln1 ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+	if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
 	else raise NotConvertible
     | _ -> raise NotConvertible
 
-and conv_eq_vect vt1 vt2 cu =
+and conv_eq_vect env vt1 vt2 cu =
   let len = Array.length vt1 in
   if Int.equal len (Array.length vt2) then
     let rcu = ref cu in
     for i = 0 to len-1 do
-      rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu
+      rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu
     done; !rcu
   else raise NotConvertible
 
 let vconv pb env t1 t2 =
   infos := create_clos_infos betaiotazeta env;
   let _cu =
-    try conv_eq pb t1 t2 (universes env)
+    try conv_eq env pb t1 t2 (universes env)
     with NotConvertible ->
       let v1 = val_of_constr env t1 in
       let v2 = val_of_constr env t2 in
-      let cu = conv_val pb (nb_rel env) v1 v2 (universes env) in
+      let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in
       cu
   in ()