Merge remote-tracking branch 'upstream/trunk' into trunk

1 files changed, 217 insertions, 59 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 427ce04c55..605e9f314c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -191,6 +191,10 @@ type 'a universe_compare =
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
     compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+      Univ.Instance.t -> int -> 'a -> 'a;
+    conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+      Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -206,6 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
    constructors. *)
 let convert_instances ~flex u u' (s, check) =
   (check.compare_instances ~flex u u' s, check)
+  
+let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
+  (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
+
+let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
+  (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -299,11 +309,11 @@ let unfold_projection infos p c =
   else None
 
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
-  eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+  eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
   Control.check_for_interrupt ();
   (* First head reduce both terms *)
   let whd = whd_stack (infos_with_reds infos betaiotazeta) in
@@ -328,13 +338,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) 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
+	       then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
                else raise NotConvertible
 	   | _ -> raise NotConvertible)
     | (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
         if Evar.equal ev1 ev2 then
-          let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
-          convert_vect l2r infos el1 el2
+          let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in
+          convert_vect env l2r infos el1 el2
             (Array.map (mk_clos env1) args1)
             (Array.map (mk_clos env2) args2) cuniv
         else raise NotConvertible
@@ -342,34 +352,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
     (* 2 index known to be bound to no constant *)
     | (FRel n, FRel m) ->
         if Int.equal (reloc_rel n el1) (reloc_rel m el2)
-        then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+        then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     (* 2 constants, 2 local defined vars or 2 defined rels *)
     | (FFlex fl1, FFlex fl2) ->
       (try
 	 let cuniv = conv_table_key infos fl1 fl2 cuniv in
-	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	   convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible | Univ.UniverseInconsistency _ ->
            (* else the oracle tells which constant is to be expanded *)
 	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
-             | Some def1 -> ((lft1, whd def1 v1), appr2)
+             | Some def1 -> ((lft1, (def1, v1)), appr2)
              | None ->
                (match unfold_reference infos fl2 with
-               | Some def2 -> (appr1, (lft2, whd def2 v2))
+               | Some def2 -> (appr1, (lft2, (def2, v2)))
 	       | None -> raise NotConvertible)
            else
 	     match unfold_reference infos fl2 with
-             | Some def2 -> (appr1, (lft2, whd def2 v2))
+             | Some def2 -> (appr1, (lft2, (def2, v2)))
              | None ->
                (match unfold_reference infos fl1 with
-               | Some def1 -> ((lft1, whd def1 v1), appr2)
+               | Some def1 -> ((lft1, (def1, v1)), appr2)
 	       | None -> raise NotConvertible) 
 	 in
-           eqappr cv_pb l2r infos app1 app2 cuniv)
+           eqappr env cv_pb l2r infos app1 app2 cuniv)
 
     | (FProj (p1,c1), FProj (p2, c2)) ->
       (* Projections: prefer unfolding to first-order unification,
@@ -377,42 +387,42 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	 form *)
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) -> 
-	eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+	eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None ->
 	match unfold_projection infos p2 c2 with
 	| Some (def2,s2) ->
-	  eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+	  eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
 	| None -> 
           if Constant.equal (Projection.constant p1) (Projection.constant p2)
 	     && compare_stack_shape v1 v2 then
-	    let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
-	      convert_stacks l2r infos lft1 lft2 v1 v2 u1
+	    let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in
+	      convert_stacks env l2r infos lft1 lft2 v1 v2 u1
 	  else (* Two projections in WHNF: unfold *)
 	    raise NotConvertible)
 
     | (FProj (p1,c1), t2) ->
       (match unfold_projection infos p1 c1 with
       | Some (def1,s1) ->
-         eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+         eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
       | None -> 
 	 (match t2 with 
 	  | FFlex fl2 ->
 	     (match unfold_reference infos fl2 with
               | Some def2 ->
-		 eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+		 eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
     | (t1, FProj (p2,c2)) ->
       (match unfold_projection infos p2 c2 with
       | Some (def2,s2) -> 
-         eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+         eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
       | None -> 
 	 (match t1 with 
 	  | FFlex fl1 ->
 	     (match unfold_reference infos fl1 with
               | Some def1 ->
-		 eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+		 eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
               | None -> raise NotConvertible)
 	  | _ -> raise NotConvertible))
       
@@ -424,15 +434,15 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
         let (_,ty1,bd1) = destFLambda mk_clos hd1 in
         let (_,ty2,bd2) = destFLambda mk_clos hd2 in
-        let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
-        ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+        let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in
+        ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
 
     | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
         if not (is_empty_stack v1 && is_empty_stack v2) then
 	  anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
 	(* Luo's system *)
-        let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
-        ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+        let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in
+        ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
 
     (* Eta-expansion on the fly *)
     | (FLambda _, _) ->
@@ -442,7 +452,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           anomaly (Pp.str "conversion was given unreduced term (FLambda).")
         in
         let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
-	eqappr CONV l2r infos
+	eqappr env CONV l2r infos
 	  (el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
     | (_, FLambda _) ->
         let () = match v2 with
@@ -451,66 +461,88 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	  anomaly (Pp.str "conversion was given unreduced term (FLambda).")
 	in
         let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
-	eqappr CONV l2r infos
+	eqappr env CONV l2r infos
 	  (el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
 	
     (* only one constant, defined var or defined rel *)
     | (FFlex fl1, c2)      ->
        (match unfold_reference infos fl1 with
 	| Some def1 ->
-	   eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+	   eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
 	| None -> 
 	   match c2 with
 	   | FConstruct ((ind2,j2),u2) ->
 	      (try
 	      let v2, v1 =
 		eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
-	      in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	      in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
 	      with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
     | (c1, FFlex fl2)      ->
        (match unfold_reference infos fl2 with
         | Some def2 ->
-	   eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+	   eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
         | None -> 
 	   match c1 with
 	   | FConstruct ((ind1,j1),u1) ->
  	      (try let v1, v2 =
 	     	     eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-	     	   in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+	     	   in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
 	       with Not_found -> raise NotConvertible)
 	   | _ -> raise NotConvertible)
        
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
-
     | (FInd (ind1,u1), FInd (ind2,u2)) ->
-        if eq_ind ind1 ind2
-	then
-	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-             convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
-        else raise NotConvertible
+      if eq_ind ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        else
+          let mind = Environ.lookup_mind (fst ind1) env in
+          let cuniv =
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              convert_instances ~flex:false u1 u2 cuniv
+            | Declarations.Cumulative_ind cumi ->
+              convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
+                u2 (CClosure.stack_args_size v2) cuniv
+          in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+      else raise NotConvertible
 
     | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
-	if Int.equal j1 j2 && eq_ind ind1 ind2
-	then
-	  (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
-           convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
-        else raise NotConvertible
+      if Int.equal j1 j2 && eq_ind ind1 ind2 then
+        if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+          let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+        else
+          let mind = Environ.lookup_mind (fst ind1) env in
+          let cuniv =
+            match mind.Declarations.mind_universes with
+            | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+              convert_instances ~flex:false u1 u2 cuniv
+            | Declarations.Cumulative_ind _ ->
+              convert_constructors
+                (mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
+                u2 (CClosure.stack_args_size v2) cuniv
+          in
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+      else raise NotConvertible
 	  
     (* Eta expansion of records *)
     | (FConstruct ((ind1,j1),u1), _) ->
       (try
     	 let v1, v2 =
     	   eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
-    	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (_, FConstruct ((ind2,j2),u2)) ->
       (try
     	 let v2, v1 =
     	   eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
-    	 in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+    	 in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
        with Not_found -> raise NotConvertible)
 
     | (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
@@ -521,11 +553,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-	  let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+	  let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-            convert_vect l2r infos
+            convert_vect env l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
     | (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -536,11 +568,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
           let fty2 = Array.map (mk_clos e2) tys2 in
           let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
           let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
-          let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+          let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
           let cuniv =
-	    convert_vect l2r infos
+	    convert_vect env l2r infos
 	      (el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
-          convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+          convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
         else raise NotConvertible
 
      (* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -551,13 +583,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
      (* In all other cases, terms are not convertible *)
      | _ -> raise NotConvertible
 
-and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
-    (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
+    (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv)
     (eq_ind)
     lft1 stk1 lft2 stk2 cuniv
 
-and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
+and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
   let lv1 = Array.length v1 in
   let lv2 = Array.length v2 in
   if Int.equal lv1 lv2
@@ -565,7 +597,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
     let rec fold n cuniv =
       if n >= lv1 then cuniv
       else
-        let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+        let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
         fold (n+1) cuniv in
     fold 0 cuniv
   else raise NotConvertible
@@ -573,7 +605,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
   let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
-  ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+  ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
 
 let check_eq univs u u' = 
@@ -610,9 +642,88 @@ let check_convert_instances ~flex u u' univs =
   if UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
+(* general conversion and inference functions *)
+let infer_check_conv_inductives
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
+    let num_param_arity =
+      mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+    in
+    if not (num_param_arity = sv1 && num_param_arity = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      infer_check_inductive_instances cv_pb cumi u1 u2 univs
+
+let infer_check_conv_constructors
+    infer_check_convert_instances
+    infer_check_inductive_instances
+    (mind, ind, cns) u1 sv1 u2 sv2 univs =
+  match mind.Declarations.mind_universes with
+  | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+    infer_check_convert_instances ~flex:false u1 u2 univs
+  | Declarations.Cumulative_ind cumi ->
+    let num_cnstr_args =
+      let nparamsctxt =
+        mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
+        (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+      nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+    in
+    if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+      infer_check_convert_instances ~flex:false u1 u2 univs
+    else
+      infer_check_inductive_instances CONV cumi u1 u2 univs
+
+let check_inductive_instances cv_pb cumi u u' univs =
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  in
+  let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+     anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.UContext.constraints
+        (Univ.subst_instance_context comp_subst ind_subtypctx)
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_cst' = 
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints 
+            (Univ.subst_instance_context comp_subst ind_subtypctx) 
+        in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    if (UGraph.check_constraints comp_cst univs) then univs
+    else raise NotConvertible
+
+let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    check_convert_instances
+    check_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let check_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    check_convert_instances
+    check_inductive_instances
+    cns u1 sv1 u2 sv2 univs
+
 let checked_universes =
   { compare = checked_sort_cmp_universes;
-    compare_instances = check_convert_instances }
+    compare_instances = check_convert_instances;
+    conv_inductives = check_conv_inductives;
+    conv_constructors = check_conv_constructors}
 
 let infer_eq (univs, cstrs as cuniv) u u' =
   if UGraph.check_eq univs u u' then cuniv
@@ -647,11 +758,58 @@ let infer_cmp_universes env pb s0 s1 univs =
         else univs
 
 let infer_convert_instances ~flex u u' (univs,cstrs) =
-  (univs, Univ.enforce_eq_instances u u' cstrs)
-
+  let cstrs' =
+    if flex then 
+      if UGraph.check_eq_instances univs u u' then cstrs
+      else raise NotConvertible
+    else Univ.enforce_eq_instances u u' cstrs
+  in (univs, cstrs')
+
+let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
+  let length_ind_instance = 
+    Univ.Instance.length
+      (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+  in
+  let ind_subtypctx =  Univ.ACumulativityInfo.subtyp_context cumi in
+  if not ((length_ind_instance = Univ.Instance.length u) &&
+          (length_ind_instance = Univ.Instance.length u')) then
+    anomaly (Pp.str "Invalid inductive subtyping encountered!")
+  else
+    let comp_cst =
+      let comp_subst = (Univ.Instance.append u u') in
+      Univ.UContext.constraints
+        (Univ.subst_instance_context comp_subst ind_subtypctx)
+    in
+    let comp_cst =
+      match cv_pb with
+        CONV -> 
+        let comp_cst' = 
+          let comp_subst = (Univ.Instance.append u' u) in
+          Univ.UContext.constraints
+            (Univ.subst_instance_context comp_subst ind_subtypctx) in
+        Univ.Constraint.union comp_cst comp_cst'
+      | CUMUL -> comp_cst
+    in
+    (univs, Univ.Constraint.union cstrs comp_cst)
+
+
+let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+  infer_check_conv_inductives
+    infer_convert_instances
+    infer_inductive_instances
+    cv_pb ind u1 sv1 u2 sv2 univs
+
+let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
+  infer_check_conv_constructors
+    infer_convert_instances
+    infer_inductive_instances
+    cns u1 sv1 u2 sv2 univs
+    
 let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
   { compare = infer_cmp_universes;
-    compare_instances = infer_convert_instances }
+    compare_instances = infer_convert_instances;
+    conv_inductives = infer_conv_inductives;
+    conv_constructors = infer_conv_constructors}
 
 let gen_conv cv_pb l2r reds env evars univs t1 t2 =
   let b =