- 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.

2 files changed, 30 insertions, 0 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 ->