Application de refresh_universes dans typing.ml et retyping.ml : les

appels à type_of et get_type_of sont souvent utilisés pour construire
des termes à partir de types; on ne rajoute pas non plus de
contraintes inutiles parce que type_of et get_type_of ne changent pas
le graphe de contraintes; tout ce qu'on perd est une information
utilisateur sur le type en lui-même mais puisque pretty.ml n'appelle
ni type_of ni get_type_of, ces informations sur la représentation
interne des univers restent a priori accessibles pour l'utilisateur.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 14 insertions, 9 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 5cc1460369..635a579c05 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -44,7 +44,7 @@ let type_of_var env id =
   with Not_found ->
     anomaly ("type_of: variable "^(string_of_id id)^" unbound")
 
-let typeur sigma metamap =
+let retype sigma metamap =
   let rec type_of env cstr=
     match kind_of_term cstr with
     | Meta n ->
@@ -132,14 +132,18 @@ let typeur sigma metamap =
   in type_of, sort_of, sort_family_of,
      type_of_global_reference_knowing_parameters
 
-let get_type_of env sigma c = let f,_,_,_ = typeur sigma [] in f env c
-let get_sort_of env sigma t = let _,f,_,_ = typeur sigma [] in f env t
-let get_sort_family_of env sigma c = let _,_,f,_ = typeur sigma [] in f env c
+let get_sort_of env sigma t = let _,f,_,_ = retype sigma [] in f env t
+let get_sort_family_of env sigma c = let _,_,f,_ = retype sigma [] in f env c
 let type_of_global_reference_knowing_parameters env sigma c args =
-  let _,_,_,f = typeur sigma [] in f env c args
+  let _,_,_,f = retype sigma [] in f env c args
 
-let get_type_of_with_meta env sigma metamap = 
-  let f,_,_,_ = typeur sigma metamap in f env
+(* We are outside the kernel: we take fresh universes *)
+(* to avoid tactics and co to refresh universes themselves *)
+let get_type_of env sigma c =
+  let f,_,_,_ = retype sigma [] in refresh_universes (f env c)
+
+let get_type_of_with_meta env sigma metamap c =
+  let f,_,_,_ = retype sigma metamap in refresh_universes (f env c)
 
 (* Makes an assumption from a constr *)
 let get_assumption_of env evc c = c
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 346942f1e8..32df490db8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -166,8 +166,9 @@ let mcheck env evd c t =
  
 let mtype_of env evd c =
   let j = execute env evd (nf_evar (evars_of evd) c) in
-  (* No normalization: it breaks Pattern! *)
-  (*nf_betaiota*) j.uj_type
+  (* We are outside the kernel: we take fresh universes *)
+  (* to avoid tactics and co to refresh universes themselves *)
+  Termops.refresh_universes j.uj_type
 
 let msort_of env evd c =
   let j = execute env evd (nf_evar (evars_of evd) c) in