- Add back some compatibility functions to avoid rewriting plugins.

- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.

5 files changed, 36 insertions, 5 deletions

diff --git a/library/universes.ml b/library/universes.ml
index f1c9c85a2..b0a610700 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -143,6 +143,8 @@ let constr_of_global gr =
 			" would forget universes."))
     else c
 
+let constr_of_reference = constr_of_global
+
 let unsafe_constr_of_global gr =
   unsafe_global_instance (Global.env ()) gr
 
@@ -205,6 +207,25 @@ let type_of_reference env r =
 
 let type_of_global t = type_of_reference (Global.env ()) t
 
+let unsafe_type_of_reference env r =
+  match r with
+  | VarRef id -> Environ.named_type id env
+  | ConstRef c ->
+     let cb = Environ.lookup_constant c env in
+       Typeops.type_of_constant_type env cb.const_type
+
+  | IndRef ind ->
+     let (mib, oib as specif) = Inductive.lookup_mind_specif env ind in
+     let (_, inst), _ = unsafe_inductive_instance env ind in
+       Inductive.type_of_inductive env (specif, inst)
+
+  | ConstructRef (ind, _ as cstr) ->
+     let (mib,oib as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in
+     let (_, inst), _ = unsafe_inductive_instance env ind in
+       Inductive.type_of_constructor (cstr,inst) specif
+
+let unsafe_type_of_global t = unsafe_type_of_reference (Global.env ()) t
+
 let fresh_sort_in_family env = function
   | InProp -> prop_sort, ContextSet.empty
   | InSet -> set_sort, ContextSet.empty
diff --git a/library/universes.mli b/library/universes.mli
index 3b951997a..4544bd4d3 100644
--- a/library/universes.mli
+++ b/library/universes.mli
@@ -144,6 +144,9 @@ val normalize_universe_subst : universe_subst ref ->
 
 val constr_of_global : Globnames.global_reference -> constr
 
+(** ** DEPRECATED ** synonym of [constr_of_global] *)
+val constr_of_reference : Globnames.global_reference -> constr
+
 (** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
     references by taking the original universe instance that is not recorded 
     anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
@@ -154,6 +157,12 @@ val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_c
     universe counter, use with care). *)
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 
+(** [unsafe_type_of_global gr] returns [gr]'s type, works on polymorphic
+    references by taking the original universe instance that is not recorded 
+    anywhere. The constraints are forgotten as well. 
+    USE with care. *)
+val unsafe_type_of_global : Globnames.global_reference -> types
+
 (** Full universes substitutions into terms *)
 
 val nf_evars_and_universes_local : (existential -> constr option) -> universe_level_subst -> 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e24c18ae2..a92698566 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -147,7 +147,8 @@ let check_conv_record (t1,sk1) (t2,sk2) =
   let c' = subst_univs_level_constr subst c in
   let t' = subst_univs_level_constr subst t' in
   let bs' = List.map (subst_univs_level_constr subst) bs in
-    ctx',t',c',bs',(Stack.append_app_list params Stack.empty,params1),
+  let f, _ = decompose_app_vect t' in
+    ctx',(t2,f),c',bs',(Stack.append_app_list params Stack.empty,params1),
     (Stack.append_app_list us Stack.empty,us2),(extra_args1,extra_args2),c1,
     (n,Stack.zip(t2,sk2))
 
@@ -668,7 +669,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
       end
 
-and conv_record trs env evd (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
+and conv_record trs env evd (ctx,(h,h'),c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
   if Reductionops.Stack.compare_shape ts ts1 then
     let (evd',ks,_,test) =
@@ -697,7 +698,7 @@ and conv_record trs env evd (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n
            us2 us);
        (fun i -> evar_conv_x trs env i CONV c1 app);
        (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
-       (fun i -> evar_conv_x trs env i CONV (substl ks t) t2)]
+       (fun i -> evar_conv_x trs env i CONV h h')]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd ((ind, i), u) l1 csts1 (c, csts2) =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index aa45b5ef1..500bb5430 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -43,7 +43,8 @@ val check_problems_are_solved : env -> evar_map -> unit
 (** Check if a canonical structure is applicable *)
 
 val check_conv_record : constr * types Stack.t -> constr * types Stack.t ->
-  Univ.universe_context_set * constr * constr * constr list * (constr Stack.t * constr Stack.t) *
+  Univ.universe_context_set * (constr * constr) 
+  * constr * constr list * (constr Stack.t * constr Stack.t) *
     (constr Stack.t * types Stack.t) *
     (constr Stack.t * types Stack.t) * constr *
     (int * constr)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 18b96e765..8e65cc480 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -507,7 +507,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t =
 	    if Int.equal npars 0 then []
 	    else
 	      try
-		let ty = evd_comb1 (Coercion.inh_coerce_to_prod loc env) evdref ty in
 	  	let IndType (indf, args) = find_rectype env !evdref ty in
 	  	let ((ind',u'),pars) = dest_ind_family indf in
 	  	  if eq_ind ind ind' then pars