Correct rebase on STM code. Thanks to E. Tassi for help on dealing with

latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.

- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-

8 files changed, 116 insertions, 97 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1db3fac52..b56d5947c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1923,11 +1923,12 @@ let eq_id avoid id =
   let hid' = next_ident_away hid avoid in
     hid'
 
-let mk_eq typ x y = mkApp (delayed_force coq_eq_ind, [| typ; x ; y |])
-let mk_eq_refl typ x = mkApp (delayed_force coq_eq_refl, [| typ; x |])
-let mk_JMeq typ x typ' y =
-  mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |])
-let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
+let mk_eq evdref typ x y = papp evdref coq_eq_ind [| typ; x ; y |]
+let mk_eq_refl evdref typ x = papp evdref coq_eq_refl [| typ; x |]
+let mk_JMeq evdref typ x typ' y =
+  papp evdref coq_JMeq_ind [| typ; x ; typ'; y |]
+let mk_JMeq_refl evdref typ x = 
+  papp evdref coq_JMeq_refl [| typ; x |]
 
 let hole = GHole (Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define true), None)
 
@@ -1987,7 +1988,7 @@ let constr_of_pat env evdref arsign pat avoid =
 		    let env = push_rel_context sign env in
 		    evdref := the_conv_x_leq (push_rel_context sign env)
 		      (lift (succ m) ty) (lift 1 apptype) !evdref;
-		    let eq_t = mk_eq (lift (succ m) ty)
+		    let eq_t = mk_eq evdref (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
 		    in
@@ -2048,7 +2049,7 @@ let rec is_included x y =
    Hence pats is already typed in its
    full signature. However prevpatterns are in the original one signature per pattern form.
  *)
-let build_ineqs prevpatterns pats liftsign =
+let build_ineqs evdref prevpatterns pats liftsign =
   let _tomatchs = List.length pats in
   let diffs =
     List.fold_left
@@ -2070,11 +2071,11 @@ let build_ineqs prevpatterns pats liftsign =
 			  lift_rel_context len ppat_sign @ sign,
 			  len',
 			  succ n, (* nth pattern *)
-			  mkApp (delayed_force coq_eq_ind,
-				[| lift (len' + liftsign) curpat_ty;
-				   liftn (len + liftsign) (succ lens) ppat_c ;
-				   lift len' curpat_c |]) ::
-			    List.map (lift lens (* Jump over this prevpat signature *)) c)
+			 (papp evdref coq_eq_ind
+			    [| lift (len' + liftsign) curpat_ty;
+			       liftn (len + liftsign) (succ lens) ppat_c ;
+			       lift len' curpat_c |]) ::
+			   List.map (lift lens (* Jump over this prevpat signature *)) c)
 		      in Some acc
 		    else None)
 	   (Some ([], 0, 0, [])) eqnpats pats
@@ -2122,7 +2123,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 		 (s, List.map (lift n) args), p) :: pats, len + n))
 	   ([], 0) pats
 	 in
-	 let ineqs = build_ineqs prevpatterns pats signlen in
+	 let ineqs = build_ineqs evdref prevpatterns pats signlen in
 	 let rhs_rels' = rels_of_patsign rhs_rels in
 	 let _signenv = push_rel_context rhs_rels' env in
 	 let arity =
@@ -2203,7 +2204,7 @@ let abstract_tomatch env tomatchs tycon =
       ([], [], [], tycon) tomatchs
   in List.rev prev, ctx, tycon
 
-let build_dependent_signature env evars avoid tomatchs arsign =
+let build_dependent_signature env evdref avoid tomatchs arsign =
   let avoid = ref avoid in
   let arsign = List.rev arsign in
   let allnames = List.rev_map (List.map pi1) arsign in
@@ -2227,19 +2228,19 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 	     let env', nargeqs, argeqs, refl_args, slift, argsign' =
 	       List.fold_left2
 		 (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
-		    let argt = Retyping.get_type_of env evars arg in
+		    let argt = Retyping.get_type_of env !evdref arg in
 		    let eq, refl_arg =
-		      if Reductionops.is_conv env evars argt t then
-			(mk_eq (lift (nargeqs + slift) argt)
+		      if Reductionops.is_conv env !evdref argt t then
+			(mk_eq evdref (lift (nargeqs + slift) argt)
 			   (mkRel (nargeqs + slift))
 			   (lift (nargeqs + nar) arg),
-			 mk_eq_refl argt arg)
+			 mk_eq_refl evdref argt arg)
 		      else
-			(mk_JMeq (lift (nargeqs + slift) t)
+			(mk_JMeq evdref (lift (nargeqs + slift) t)
 			   (mkRel (nargeqs + slift))
 			   (lift (nargeqs + nar) argt)
 			   (lift (nargeqs + nar) arg),
-			 mk_JMeq_refl argt arg)
+			 mk_JMeq_refl evdref argt arg)
 		    in
 		    let previd, id =
 		      let name =
@@ -2256,13 +2257,13 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 		       (Name id, b, t) :: argsign'))
 		 (env, neqs, [], [], slift, []) args argsign
 	     in
-	     let eq = mk_JMeq
+	     let eq = mk_JMeq evdref
 	       (lift (nargeqs + slift) appt)
 	       (mkRel (nargeqs + slift))
 	       (lift (nargeqs + nar) ty)
 	       (lift (nargeqs + nar) tm)
 	     in
-	     let refl_eq = mk_JMeq_refl ty tm in
+	     let refl_eq = mk_JMeq_refl evdref ty tm in
 	     let previd, id = make_prime avoid appn in
 	       (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
 		succ nargeqs,
@@ -2276,11 +2277,11 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 	     let arsign' = (Name id, b, typ) in
 	     let tomatch_ty = type_of_tomatch ty in
 	     let eq =
-	       mk_eq (lift nar tomatch_ty)
+	       mk_eq evdref (lift nar tomatch_ty)
 		 (mkRel slift) (lift nar tm)
 	     in
 	       ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
-		(mk_eq_refl tomatch_ty tm) :: refl_args,
+		(mk_eq_refl evdref tomatch_ty tm) :: refl_args,
 		pred slift, (arsign' :: []) :: arsigns))
       ([], 0, [], nar, []) tomatchs arsign
   in
@@ -2317,7 +2318,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
       (* Build the dependent arity signature, the equalities which makes
 	 the first part of the predicate and their instantiations. *)
     let avoid = [] in
-      build_dependent_signature env ( !evdref) avoid tomatchs arsign
+      build_dependent_signature env evdref avoid tomatchs arsign
 
   in
   let tycon, arity =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 43af6ec62..c7173c2d1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -28,6 +28,7 @@ open Evarutil
 open Evarconv
 open Evd
 open Termops
+open Globnames
 
 (* Typing operations dealing with coercions *)
 exception NoCoercion
@@ -84,7 +85,7 @@ let disc_subset x =
        Ind (i,_) ->
 	 let len = Array.length l in
 	 let sigty = delayed_force sig_typ in
-	   if Int.equal len 2 && eq_ind i (fst (Term.destInd sigty))
+	   if Int.equal len 2 && eq_ind i (Globnames.destIndRef sigty)
 	   then
 	     let (a, b) = pair_of_array l in
 	       Some (a, b)
@@ -113,8 +114,7 @@ let mu env evdref t =
 	let p = hnf_nodelta env !evdref p in
 	  (Some (fun x ->
 		   app_opt env evdref 
-		     f (mkApp (delayed_force sig_proj1,
-			       [| u; p; x |]))),
+		     f (papp evdref sig_proj1 [| u; p; x |])),
 	   ct)
       | None -> (None, v)
   in aux t
@@ -158,10 +158,11 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		in
 		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
-		let eq = mkApp (delayed_force coq_eq_ind, [| eqT; hdx; hdy |]) in
+		let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
 		let evar = make_existential loc env evdref eq in
-		let eq_app x = mkApp (delayed_force coq_eq_rect,
-				      [| eqT; hdx; pred; x; hdy; evar|]) in
+		let eq_app x = papp evdref coq_eq_rect
+		  [| eqT; hdx; pred; x; hdy; evar|] 
+		in
 		  aux (hdy :: tele) (subst1 hdx restT) 
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some co
@@ -204,9 +205,9 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 	     let prod = delayed_force prod_typ in
 	       (* Sigma types *)
 	       if Int.equal len (Array.length l') && Int.equal len 2 && eq_ind i i'
-		 && (eq_ind i (fst (Term.destInd sigT)) || eq_ind i (fst (Term.destInd prod)))
+		 && (eq_ind i (destIndRef sigT) || eq_ind i (destIndRef prod))
 	       then
-		 if eq_ind i (fst (Term.destInd sigT))
+		 if eq_ind i (destIndRef sigT)
 		 then
 		   begin
 		     let (a, pb), (a', pb') =
@@ -238,12 +239,12 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 			   Some
 			     (fun x ->
 				let x, y =
-				  app_opt env' evdref c1 (mkApp (delayed_force sigT_proj1,
-								  [| a; pb; x |])),
-				  app_opt env' evdref c2 (mkApp (delayed_force sigT_proj2,
-								  [| a; pb; x |]))
+				  app_opt env' evdref c1 (papp evdref sigT_proj1
+							    [| a; pb; x |]),
+				  app_opt env' evdref c2 (papp evdref sigT_proj2
+							  [| a; pb; x |])
 				in
-				  mkApp (delayed_force sigT_intro, [| a'; pb'; x ; y |]))
+				  papp evdref sigT_intro [| a'; pb'; x ; y |])
 		   end
 		 else
 		   begin
@@ -258,12 +259,12 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 			   Some
 			     (fun x ->
 				let x, y =
-				  app_opt env evdref c1 (mkApp (delayed_force prod_proj1,
-								 [| a; b; x |])),
-				  app_opt env evdref c2 (mkApp (delayed_force prod_proj2,
-								 [| a; b; x |]))
+				  app_opt env evdref c1 (papp evdref prod_proj1
+							   [| a; b; x |]),
+				  app_opt env evdref c2 (papp evdref prod_proj2
+							   [| a; b; x |])
 				in
-				  mkApp (delayed_force prod_intro, [| a'; b'; x ; y |]))
+				  papp evdref prod_intro [| a'; b'; x ; y |])
 		   end
 	       else
 		 if eq_ind i i' && Int.equal len (Array.length l') then
@@ -294,8 +295,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
     Some (u, p) ->
       let c = coerce_unify env u y in
       let f x =
-	app_opt env evdref c (mkApp (delayed_force sig_proj1,
-				      [| u; p; x |]))
+	app_opt env evdref c (papp evdref sig_proj1 [| u; p; x |])
       in Some f
     | None ->
 	match disc_subset y with
@@ -306,9 +306,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		 let cx = app_opt env evdref c x in
 		 let evar = make_existential loc env evdref (mkApp (p, [| cx |]))
 		 in
-		   (mkApp
-		      (delayed_force sig_intro,
-		       [| u; p; cx; evar |])))
+		   (papp evdref sig_intro [| u; p; cx; evar |]))
 	| None ->
 	    raise NoSubtacCoercion
   in coerce_unify env x y
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index b3c65ebaf..306116d76 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1082,10 +1082,16 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar
       let evi2 = Evd.find evd evk2 in
       let evi2env = Evd.evar_env evi2 in
       let ctx', j = Reduction.dest_arity evi2env evi2.evar_concl in
-	if i == j || Evd.check_eq evd (univ_of_sort i) (univ_of_sort j) 
+      let ui, uj = univ_of_sort i, univ_of_sort j in
+	if i == j || Evd.check_eq evd ui uj
 	then (* Shortcut, i = j *) 
 	  solve_evar_evar ~force f g env evd pbty ev1 ev2
-	else 
+	  (* Avoid looping if postponing happened on previous evar/evar problem *) 
+	else if Evd.check_leq evd ui uj then
+	  solve_evar_evar ~force f g env evd None ev1 ev2
+	else if Evd.check_leq evd uj ui then
+	  solve_evar_evar ~force f g env evd None ev2 ev1
+	else
 	  let evd, k = Evd.new_sort_variable univ_flexible_alg evd in
 	  let evd, ev3 = 
 	    Evarutil.new_pure_evar evd (Evd.evar_hyps evi) 
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0776988d7..ae16fbebe 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1005,14 +1005,6 @@ let fresh_constructor_instance env evd c =
   with_context_set univ_flexible evd (Universes.fresh_constructor_instance env c)
 
 let fresh_global ?(rigid=univ_flexible) env evd gr =
-  (* match gr with *)
-  (* | ConstructRef c -> let evd, c = fresh_constructor_instance env evd c in  *)
-  (* 			evd, mkConstructU c *)
-  (* | IndRef c -> let evd, c = fresh_inductive_instance env evd c in *)
-  (* 		  evd, mkIndU c *)
-  (* | ConstRef c -> let evd, c = fresh_constant_instance env evd c in *)
-  (* 		    evd, mkConstU c *)
-  (* | VarRef i -> evd, mkVar i *)
   with_context_set rigid evd (Universes.fresh_global_instance env gr)
 
 let whd_sort_variable evd t = t
@@ -1420,6 +1412,9 @@ type 'a sigma = {
 
 let sig_it x = x.it
 let sig_sig x = x.sigma
+let on_sig s f = 
+  let sigma', v = f s.sigma in
+    { s with sigma = sigma' }, v
 
 (*******************************************************************)
 (* The state monad with state an evar map. *)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 18d68bebf..e44e8e906 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -226,7 +226,8 @@ val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 (** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 
-val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map ->  evar_map -> evar_map
+val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool -> 
+  evar_map ->  evar_map -> evar_map
 (** spiwack: this function seems to somewhat break the abstraction. *)
 
 (** {6 Misc} *)
@@ -283,12 +284,14 @@ type 'a sigma = {
 
 val sig_it  : 'a sigma -> 'a
 val sig_sig : 'a sigma -> evar_map
+val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b
 
 (** {5 The state monad with state an evar map} *)
 
 module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a
 module Monad  : Monad.S with type +'a t = evar_map -> 'a * evar_map
 
+
 (** {5 Meta machinery}
 
     These functions are almost deprecated. They were used before the
@@ -478,7 +481,8 @@ val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstan
 val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive
 val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor
 
-val fresh_global : ?rigid:rigid -> env -> evar_map -> Globnames.global_reference -> evar_map * constr
+val fresh_global : ?rigid:rigid -> env -> evar_map -> 
+  Globnames.global_reference -> evar_map * constr
 
 (********************************************************************
   Conversion w.r.t. an evar map: might generate universe unifications 
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 67bb3bd2a..a0ecfb1f9 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -26,27 +26,31 @@ let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr
 let init_constant dir s () = coq_constant "Program" dir s
 let init_reference dir s () = coq_reference "Program" dir s
 
-let sig_typ = init_constant ["Init"; "Specif"] "sig"
-let sig_intro = init_constant ["Init"; "Specif"] "exist"
-let sig_proj1 = init_constant ["Init"; "Specif"] "proj1_sig"
+let papp evdref r args = 
+  let gr = delayed_force r in
+    mkApp (Evarutil.e_new_global evdref gr, args)
 
-let sigT_typ = init_constant ["Init"; "Specif"] "sigT"
-let sigT_intro = init_constant ["Init"; "Specif"] "existT"
-let sigT_proj1 = init_constant ["Init"; "Specif"] "projT1"
-let sigT_proj2 = init_constant ["Init"; "Specif"] "projT2"
+let sig_typ = init_reference ["Init"; "Specif"] "sig"
+let sig_intro = init_reference ["Init"; "Specif"] "exist"
+let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig"
 
-let prod_typ = init_constant ["Init"; "Datatypes"] "prod"
-let prod_intro = init_constant ["Init"; "Datatypes"] "pair"
-let prod_proj1 = init_constant ["Init"; "Datatypes"] "fst"
-let prod_proj2 = init_constant ["Init"; "Datatypes"] "snd"
+let sigT_typ = init_reference ["Init"; "Specif"] "sigT"
+let sigT_intro = init_reference ["Init"; "Specif"] "existT"
+let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1"
+let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2"
 
-let coq_eq_ind = init_constant ["Init"; "Logic"] "eq"
-let coq_eq_refl = init_constant ["Init"; "Logic"] "eq_refl"
+let prod_typ = init_reference ["Init"; "Datatypes"] "prod"
+let prod_intro = init_reference ["Init"; "Datatypes"] "pair"
+let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst"
+let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd"
+
+let coq_eq_ind = init_reference ["Init"; "Logic"] "eq"
+let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl"
 let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl"
-let coq_eq_rect = init_constant ["Init"; "Logic"] "eq_rect"
+let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect"
 
-let coq_JMeq_ind = init_constant ["Logic";"JMeq"] "JMeq"
-let coq_JMeq_refl = init_constant ["Logic";"JMeq"] "JMeq_refl"
+let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq"
+let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl"
 
 let coq_not = init_constant ["Init";"Logic"] "not"
 let coq_and = init_constant ["Init";"Logic"] "and"
diff --git a/pretyping/program.mli b/pretyping/program.mli
index 0572a93a0..5b40b2e71 100644
--- a/pretyping/program.mli
+++ b/pretyping/program.mli
@@ -7,29 +7,33 @@
 (************************************************************************)
 
 open Term
+open Globnames
 
 (** A bunch of Coq constants used by Progam *)
 
-val sig_typ : unit -> constr
-val sig_intro : unit -> constr
-val sig_proj1 : unit -> constr
-val sigT_typ : unit -> constr
-val sigT_intro : unit -> constr
-val sigT_proj1 : unit -> constr
-val sigT_proj2 : unit -> constr
+val sig_typ : unit -> global_reference
+val sig_intro : unit -> global_reference
+val sig_proj1 : unit -> global_reference
+val sigT_typ : unit -> global_reference
+val sigT_intro : unit -> global_reference
+val sigT_proj1 : unit -> global_reference
+val sigT_proj2 : unit -> global_reference
 
-val prod_typ : unit -> constr
-val prod_intro : unit -> constr
-val prod_proj1 : unit -> constr
-val prod_proj2 : unit -> constr
+val prod_typ : unit -> global_reference
+val prod_intro : unit -> global_reference
+val prod_proj1 : unit -> global_reference
+val prod_proj2 : unit -> global_reference
 
-val coq_eq_ind : unit -> constr
-val coq_eq_refl : unit -> constr
-val coq_eq_refl_ref : unit -> Globnames.global_reference
-val coq_eq_rect : unit -> constr
+val coq_eq_ind : unit -> global_reference
+val coq_eq_refl : unit -> global_reference
+val coq_eq_refl_ref : unit -> global_reference
+val coq_eq_rect : unit -> global_reference
 
-val coq_JMeq_ind : unit -> constr
-val coq_JMeq_refl : unit -> constr
+val coq_JMeq_ind : unit -> global_reference
+val coq_JMeq_refl : unit -> global_reference
 
 val mk_coq_and : constr list -> constr
 val mk_coq_not : constr -> constr
+
+(** Polymorphic application of delayed references *)
+val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index fac73670b..fdcce914d 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -255,8 +255,10 @@ let build_subclasses ~check env sigma glob pri =
       (fun () -> incr i;
         Nameops.add_suffix _id ("_subinstance_" ^ string_of_int !i))
   in
-  let rec aux pri c path =
-    let ty = Evarutil.nf_evar sigma (Retyping.get_type_of env sigma c) in
+  let ty, ctx = Global.type_of_global_in_context env glob in
+  let sigma = Evd.merge_context_set Evd.univ_rigid sigma (Univ.ContextSet.of_context ctx) in
+  let rec aux pri c ty path =
+    let ty = Evarutil.nf_evar sigma ty in
       match class_of_constr ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
@@ -284,10 +286,15 @@ let build_subclasses ~check env sigma glob pri =
 	in
 	let declare_proj hints (cref, pri, body) =
 	  let path' = cref :: path in
-	  let rest = aux pri body path' in
+	  let ty = Retyping.get_type_of env sigma body in
+	  let rest = aux pri body ty path' in
 	    hints @ (path', pri, body) :: rest
 	in List.fold_left declare_proj [] projs 
-  in aux pri (Universes.constr_of_global glob) [glob]
+  in
+  let term = Universes.constr_of_global_univ (glob,Univ.UContext.instance ctx) in
+    (*FIXME subclasses should now get substituted for each particular instance of
+      the polymorphic superclass *)
+    aux pri term ty [glob]
 
 (*
  * instances persistent object