Imported Upstream version 8.5~beta1+dfsg

1 files changed, 178 insertions, 119 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 5a8d537e..8643fe10 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -44,9 +44,12 @@
    natural expectation of the user.
 *)
 
+open Errors
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
 open Environ
 open Inductive
@@ -56,16 +59,18 @@ open Inductiveops
 open Ind_tables
 open Indrec
 
-let hid = id_of_string "H"
-let xid = id_of_string "X"
+let hid = Id.of_string "H"
+let xid = Id.of_string "X"
 let default_id_of_sort = function InProp | InSet -> hid | InType -> xid
 let fresh env id = next_global_ident_away id []
+let with_context_set ctx (b, ctx') = 
+  (b, Univ.ContextSet.union ctx ctx')
 
 let build_dependent_inductive ind (mib,mip) =
-  let realargs,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
+  let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
-    (mkInd ind,
-       extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt
+    (mkIndU ind,
+       extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
        @ extended_rel_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
@@ -73,12 +78,13 @@ let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
 let my_it_mkLambda_or_LetIn_name s c =
   it_mkLambda_or_LetIn_name (Global.env()) c s
 
-let get_coq_eq () =
+let get_coq_eq ctx =
   try
-    let eq = Libnames.destIndRef Coqlib.glob_eq in
-    let _ = Global.lookup_inductive eq in
+    let eq = Globnames.destIndRef Coqlib.glob_eq in
     (* Do not force the lazy if they are not defined *)
-    mkInd eq, Coqlib.build_coq_eq_refl ()
+    let eq, ctx = with_context_set ctx 
+      (Universes.fresh_inductive_instance (Global.env ()) eq) in
+      mkIndU eq, mkConstructUi (eq,1), ctx
   with Not_found ->
     error "eq not found."
 
@@ -91,27 +97,30 @@ let get_coq_eq () =
 (* in which case, a symmetry lemma is definable                       *)
 (**********************************************************************)
 
-let get_sym_eq_data env ind =
+let get_sym_eq_data env (ind,u) =
   let (mib,mip as specif) = lookup_mind_specif env ind in
-  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+  if not (Int.equal (Array.length mib.mind_packets) 1) ||
+    not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
-  if List.exists (fun (_,b,_) -> b <> None) realsign then
+  let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
+  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
-  let params,constrargs = list_chop mib.mind_nparams constrargs in
+  let params,constrargs = List.chop mib.mind_nparams constrargs in
   if mip.mind_nrealargs > mib.mind_nparams then
     error "Constructors arguments must repeat the parameters.";
-  let _,params2 = list_chop (mib.mind_nparams-mip.mind_nrealargs) params in
+  let _,params2 = List.chop (mib.mind_nparams-mip.mind_nrealargs) params in
+  let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
   let paramsctxt1,_ =
-    list_chop (mib.mind_nparams-mip.mind_nrealargs) mib.mind_params_ctxt in
-  if not (list_equal eq_constr params2 constrargs) then
+    List.chop (mib.mind_nparams-mip.mind_nrealargs) paramsctxt in
+  if not (List.equal eq_constr params2 constrargs) then
     error "Constructors arguments must repeat the parameters.";
   (* nrealargs_ctxt and nrealargs are the same here *)
-  (specif,mip.mind_nrealargs,realsign,mib.mind_params_ctxt,paramsctxt1)
+  (specif,mip.mind_nrealargs,realsign,paramsctxt,paramsctxt1)
 
 (**********************************************************************)
 (* Check if an inductive type [ind] has the form                      *)
@@ -123,19 +132,23 @@ let get_sym_eq_data env ind =
 (* such that symmetry is a priori definable                           *)
 (**********************************************************************)
 
-let get_non_sym_eq_data env ind =
+let get_non_sym_eq_data env (ind,u) =
   let (mib,mip as specif) = lookup_mind_specif env ind in
-  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+  if not (Int.equal (Array.length mib.mind_packets) 1) ||
+    not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
-  if List.exists (fun (_,b,_) -> b <> None) realsign then
+  let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
+  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
-  let _,constrargs = list_chop mib.mind_nparams constrargs in
-  (specif,constrargs,realsign,mip.mind_nrealargs)
+  let _,constrargs = List.chop mib.mind_nparams constrargs in
+  let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
+  let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
+  (specif,constrargs,realsign,paramsctxt,mip.mind_nrealargs)
 
 (**********************************************************************)
 (* Build the symmetry lemma associated to an inductive type           *)
@@ -152,30 +165,35 @@ let get_non_sym_eq_data env ind =
 (**********************************************************************)
 
 let build_sym_scheme env ind =
+  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
-    get_sym_eq_data env ind in
+    get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let applied_ind = build_dependent_inductive ind specif in
+  let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
+  let c = 
   (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
   (mkCase (ci,
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
-       (mkApp (mkInd ind,Array.concat
+       (mkApp (mkIndU indu,Array.concat
 	  [extended_rel_vect (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
        [|cstr (nrealargs+1)|]))))
+  in c, Evd.evar_universe_context_of ctx
 
 let sym_scheme_kind =
   declare_individual_scheme_object "_sym_internal"
-  (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind)
+  (fun ind -> 
+    let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in
+      (c, ctx), Declareops.no_seff)
 
 (**********************************************************************)
 (* Build the involutivity of symmetry for an inductive type           *)
@@ -193,49 +211,59 @@ let sym_scheme_kind =
 (*                                                                    *)
 (**********************************************************************)
 
+let const_of_scheme kind env ind ctx = 
+  let sym_scheme, eff = (find_scheme kind ind) in
+  let sym, ctx = with_context_set ctx 
+    (Universes.fresh_constant_instance (Global.env()) sym_scheme) in
+    mkConstU sym, ctx, eff
+
 let build_sym_involutive_scheme env ind =
+  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
-    get_sym_eq_data env ind in
-  let sym = mkConst (find_scheme sym_scheme_kind ind) in
-  let (eq,eqrefl) = get_coq_eq () in
-  let cstr n = mkApp (mkConstruct(ind,1),extended_rel_vect n paramsctxt) in
+    get_sym_eq_data env indu in
+  let eq,eqrefl,ctx = get_coq_eq ctx in
+  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
+  let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let applied_ind = build_dependent_inductive ind specif in
+  let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
-      (mkInd ind, Array.append
+      (mkIndU indu, Array.append
          (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
   let ci = make_case_info (Global.env()) ind RegularStyle in
-  (my_it_mkLambda_or_LetIn paramsctxt
-  (my_it_mkLambda_or_LetIn_name realsign_ind
-  (mkCase (ci,
-     my_it_mkLambda_or_LetIn_name
-       (lift_rel_context (nrealargs+1) realsign_ind)
-       (mkApp (eq,[|
-	 mkApp
-	   (mkInd ind, Array.concat
-	     [extended_rel_vect (3*nrealargs+2) paramsctxt1;
-	      rel_vect (2*nrealargs+2) nrealargs;
-	      rel_vect 1 nrealargs]);
-         mkApp (sym,Array.concat
-	   [extended_rel_vect (3*nrealargs+2) paramsctxt1;
-            rel_vect 1 nrealargs;
-            rel_vect (2*nrealargs+2) nrealargs;
-            [|mkApp (sym,Array.concat
-	      [extended_rel_vect (3*nrealargs+2) paramsctxt1;
-	       rel_vect (2*nrealargs+2) nrealargs;
-	       rel_vect 1 nrealargs;
-	       [|mkRel 1|]])|]]);
-	 mkRel 1|])),
-     mkRel 1 (* varH *),
-       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+  let c = 
+    (my_it_mkLambda_or_LetIn paramsctxt
+     (my_it_mkLambda_or_LetIn_name realsign_ind
+      (mkCase (ci,
+	       my_it_mkLambda_or_LetIn_name
+	       (lift_rel_context (nrealargs+1) realsign_ind)
+	       (mkApp (eq,[|
+	       mkApp
+	       (mkIndU indu, Array.concat
+	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		rel_vect (2*nrealargs+2) nrealargs;
+		rel_vect 1 nrealargs]);
+               mkApp (sym,Array.concat
+	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		rel_vect 1 nrealargs;
+		rel_vect (2*nrealargs+2) nrealargs;
+		[|mkApp (sym,Array.concat
+		[extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		 rel_vect (2*nrealargs+2) nrealargs;
+		 rel_vect 1 nrealargs;
+		 [|mkRel 1|]])|]]);
+	       mkRel 1|])),
+	       mkRel 1 (* varH *),
+	       [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+  in (c, Evd.evar_universe_context_of ctx), eff
 
 let sym_involutive_scheme_kind =
   declare_individual_scheme_object "_sym_involutive"
-  (fun ind -> build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
+  (fun ind -> 
+    build_sym_involutive_scheme (Global.env() (* side-effect! *)) ind)
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for conclusion associated  *)
@@ -298,26 +326,27 @@ let sym_involutive_scheme_kind =
 (**********************************************************************)
 
 let build_l2r_rew_scheme dep env ind kind =
+  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
-    get_sym_eq_data env ind in
-  let sym = mkConst (find_scheme sym_scheme_kind ind) in
-  let sym_involutive = mkConst (find_scheme sym_involutive_scheme_kind ind) in
-  let (eq,eqrefl) = get_coq_eq () in
+    get_sym_eq_data env indu in
+  let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
+  let sym_involutive, ctx, eff' = const_of_scheme sym_involutive_scheme_kind env ind ctx in
+  let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
-    mkApp (mkConstruct(ind,1),
+    mkApp (mkConstructUi(indu,1),
       Array.concat [extended_rel_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
-  let applied_ind = build_dependent_inductive ind specif in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
+  let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
-    mkApp (mkInd ind, Array.concat
+    mkApp (mkIndU indu, Array.concat
        [extended_rel_vect (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
-    mkApp (mkInd ind, Array.concat
+    mkApp (mkIndU indu, Array.concat
        [extended_rel_vect (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
@@ -336,9 +365,11 @@ let build_l2r_rew_scheme dep env ind kind =
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
-  let s = mkSort (new_sort_in_family kind) in
+  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let ctx = Univ.ContextSet.union ctx ctx' in
+  let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
-  let cieq = make_case_info (Global.env()) (destInd eq) RegularStyle in
+  let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
@@ -363,6 +394,7 @@ let build_l2r_rew_scheme dep env ind kind =
       my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
       applied_sym_C 3,
       [|mkVar varHC|]) in
+  let c = 
   (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
   (my_it_mkLambda_or_LetIn_name realsign
   (mkNamedLambda varP
@@ -380,6 +412,7 @@ let build_l2r_rew_scheme dep env ind kind =
        [|main_body|])
    else
      main_body))))))
+  in (c, Evd.evar_universe_context_of ctx), Declareops.union_side_effects eff' eff
 
 (**********************************************************************)
 (* Build the left-to-right rewriting lemma for hypotheses associated  *)
@@ -408,23 +441,24 @@ let build_l2r_rew_scheme dep env ind kind =
 (**********************************************************************)
 
 let build_l2r_forward_rew_scheme dep env ind kind =
+  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
-    get_sym_eq_data env ind in
+    get_sym_eq_data env indu in
   let cstr n p =
-    mkApp (mkConstruct(ind,1),
+    mkApp (mkConstructUi(indu,1),
       Array.concat [extended_rel_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
-  let applied_ind = build_dependent_inductive ind specif in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
+  let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
-    mkApp (mkInd ind, Array.concat
+    mkApp (mkIndU indu, Array.concat
        [extended_rel_vect (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
-    mkApp (mkInd ind, Array.concat
+    mkApp (mkIndU indu, Array.concat
        [extended_rel_vect (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
@@ -433,7 +467,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
   let realsign_ind_P n aP =
     name_context env ((Name varH,None,aP)::realsign_P n) in
-  let s = mkSort (new_sort_in_family kind) in
+  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let ctx = Univ.ContextSet.union ctx ctx' in
+  let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let applied_PC =
     mkApp (mkVar varP,Array.append
@@ -447,6 +483,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 3 nrealargs)
            (if dep then [|cstr (3*nrealargs+4) 3|] else [||])) in
+  let c = 
   (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
   (my_it_mkLambda_or_LetIn_name realsign
   (mkNamedLambda varH applied_ind
@@ -463,6 +500,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 	  (if dep then realsign_ind_P 1 applied_ind_P' else realsign_P 2) s)
       (mkNamedLambda varHC applied_PC'
 	(mkVar varHC))|])))))
+  in c, Evd.evar_universe_context_of ctx
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for hypotheses associated  *)
@@ -494,19 +532,22 @@ let build_l2r_forward_rew_scheme dep env ind kind =
 (* statement but no need for symmetry of the equality.                *)
 (**********************************************************************)
 
-let build_r2l_forward_rew_scheme dep env ind kind =
-  let ((mib,mip as specif),constrargs,realsign,nrealargs) =
-    get_non_sym_eq_data env ind in
+let build_r2l_forward_rew_scheme dep env ind kind = 
+  let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in
+  let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
+    get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstruct(ind,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
-  let varHC = fresh env (id_of_string "HC") in
-  let varP = fresh env (id_of_string "P") in
-  let applied_ind = build_dependent_inductive ind specif in
+  let varHC = fresh env (Id.of_string "HC") in
+  let varP = fresh env (Id.of_string "P") in
+  let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
-  let s = mkSort (new_sort_in_family kind) in
+  let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in
+  let ctx = Univ.ContextSet.union ctx ctx' in
+  let s = mkSort s in
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let applied_PC =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
@@ -514,7 +555,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     mkApp (mkVar varP,
            if dep then extended_rel_vect 0 realsign_ind
 	   else extended_rel_vect 1 realsign) in
-  (my_it_mkLambda_or_LetIn mib.mind_params_ctxt
+  let c = 
+  (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
   (mkNamedLambda varP
     (my_it_mkProd_or_LetIn (lift_rel_context (nrealargs+1)
@@ -531,6 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
 	   lift (nrealargs+3) applied_PC,
 	   mkRel 1)|]),
     [|mkVar varHC|]))))))
+  in c, Evd.evar_universe_context_of ctx
 
 (**********************************************************************)
 (* This function "repairs" the non-dependent r2l forward rewriting    *)
@@ -548,11 +591,12 @@ let build_r2l_forward_rew_scheme dep env ind kind =
 (*                                                                    *)
 (**********************************************************************)
 
-let fix_r2l_forward_rew_scheme c =
+let fix_r2l_forward_rew_scheme (c, ctx') =
   let t = Retyping.get_type_of (Global.env()) Evd.empty c in
   let ctx,_ = decompose_prod_assum t in
   match ctx with
   | hp :: p :: ind :: indargs ->
+     let c' = 
       my_it_mkLambda_or_LetIn indargs
 	(mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
 	  (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
@@ -560,7 +604,8 @@ let fix_r2l_forward_rew_scheme c =
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
 	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
-  | _ -> anomaly "Ill-formed non-dependent left-to-right rewriting scheme"
+      in c', ctx'
+  | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
 (**********************************************************************)
 (* Build the right-to-left rewriting lemma for conclusion associated  *)
@@ -582,9 +627,16 @@ let fix_r2l_forward_rew_scheme c =
 (*          (H:I q1..qm a1..an),                                      *)
 (*          P b1..bn C -> P a1..an H                                  *)
 (**********************************************************************)
-
+ 
 let build_r2l_rew_scheme dep env ind k =
-  build_case_analysis_scheme env Evd.empty ind dep k
+  let sigma, indu = Evd.fresh_inductive_instance env (Evd.from_env env) ind in
+  let sigma', c = build_case_analysis_scheme env sigma indu dep k in
+    c, Evd.evar_universe_context sigma'
+
+let build_l2r_rew_scheme = build_l2r_rew_scheme
+let build_l2r_forward_rew_scheme = build_l2r_forward_rew_scheme
+let build_r2l_rew_scheme = build_r2l_rew_scheme
+let build_r2l_forward_rew_scheme = build_r2l_forward_rew_scheme
 
 (**********************************************************************)
 (* Register the rewriting schemes                                     *)
@@ -608,7 +660,7 @@ let rew_l2r_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_dep_scheme_kind =
   declare_individual_scheme_object "_rew_dep"
-  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from right-to-left in hypotheses                 *)
@@ -618,7 +670,7 @@ let rew_r2l_dep_scheme_kind =
 (**********************************************************************)
 let rew_r2l_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_dep"
-  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Dependent rewrite from left-to-right in hypotheses                 *)
@@ -628,7 +680,7 @@ let rew_r2l_forward_dep_scheme_kind =
 (**********************************************************************)
 let rew_l2r_forward_dep_scheme_kind =
   declare_individual_scheme_object "_rew_fwd_r_dep"
-  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
+  (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either left-to-right in conclusion or   *)
@@ -642,7 +694,7 @@ let rew_l2r_forward_dep_scheme_kind =
 let rew_l2r_scheme_kind =
   declare_individual_scheme_object "_rew_r"
   (fun ind -> fix_r2l_forward_rew_scheme
-      (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
+     (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
 
 (**********************************************************************)
 (* Non-dependent rewrite from either right-to-left in conclusion or   *)
@@ -652,7 +704,7 @@ let rew_l2r_scheme_kind =
 (**********************************************************************)
 let rew_r2l_scheme_kind =
   declare_individual_scheme_object "_rew"
-  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
+  (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
 
 (* End of rewriting schemes *)
 
@@ -671,35 +723,41 @@ let rew_r2l_scheme_kind =
 
 (* TODO: extend it to types with more than one index *)
 
-let build_congr env (eq,refl) ind =
+let build_congr env (eq,refl,ctx) ind =
+  let (ind,u as indu), ctx = with_context_set ctx 
+    (Universes.fresh_inductive_instance env ind) in
   let (mib,mip) = lookup_mind_specif env ind in
-  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
+  if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then
     error "Not an inductive type with a single constructor.";
-  if mip.mind_nrealargs <> 1 then
+  if not (Int.equal mip.mind_nrealargs 1) then
     error "Expect an inductive type with one predicate parameter.";
   let i = 1 in
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
-  if List.exists (fun (_,b,_) -> b <> None) realsign then
+  let arityctxt = Vars.subst_instance_context u mip.mind_arity_ctxt in
+  let paramsctxt = Vars.subst_instance_context u mib.mind_params_ctxt in
+  let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in
+  if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then
     error "Inductive equalities with local definitions in arity not supported.";
-  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
+  let env_with_arity = push_rel_context arityctxt env in
   let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
+  if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
-  let varB = fresh env (id_of_string "B") in
-  let varH = fresh env (id_of_string "H") in
-  let varf = fresh env (id_of_string "f") in
+  let varB = fresh env (Id.of_string "B") in
+  let varH = fresh env (Id.of_string "H") in
+  let varf = fresh env (Id.of_string "f") in
   let ci = make_case_info (Global.env()) ind RegularStyle in
-  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
-     (mkNamedLambda varB (new_Type ())
+  let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in
+  let c = 
+  my_it_mkLambda_or_LetIn paramsctxt
+     (mkNamedLambda varB (mkSort (Type uni))
      (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
      (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
      (mkNamedLambda varH
         (applist
-           (mkInd ind,
-	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
+           (mkIndU indu,
+	    extended_rel_list (mip.mind_nrealargs+2) paramsctxt @
 	    extended_rel_list 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
@@ -707,20 +765,21 @@ let build_congr env (eq,refl) ind =
          (mkLambda
            (Anonymous,
             applist
-             (mkInd ind,
-	        extended_rel_list (2*mip.mind_nrealargs_ctxt+3)
-		  mib.mind_params_ctxt
+             (mkIndU indu,
+	        extended_rel_list (2*mip.mind_nrealdecls+3)
+		  paramsctxt
 	        @ extended_rel_list 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
-                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) b|]);
+                mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
 		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
        mkVar varH,
        [|mkApp (refl,
           [|mkVar varB;
 	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) b|])|])|]))))))
+  in c, Evd.evar_universe_context_of ctx
 
 let congr_scheme_kind = declare_individual_scheme_object "_congr"
   (fun ind ->
     (* May fail if equality is not defined *)
-    build_congr (Global.env()) (get_coq_eq ()) ind)
+    build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, Declareops.no_seff)