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

1 files changed, 4 insertions, 8 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3e79c6f0..7a885687d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -656,7 +656,6 @@ let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
     match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
       | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
-	  let c2 = refresh_universes c2 in
 	  tclTHENLAST
 	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
 	    (apply_term c [mkMeta (new_meta())]) gl
@@ -1050,7 +1049,7 @@ let true_cut = assert_tac true
 (**************************)
 
 let generalize_goal gl c cl =
-  let t = refresh_universes (pf_type_of gl c) in
+  let t = pf_type_of gl c in
   match kind_of_term c with
     | Var id ->
 	(* The choice of remembering or not a non dependent name has an impact
@@ -1242,7 +1241,7 @@ let letin_tac with_eq name c occs gl =
       if not (mem_named_context x (pf_hyps gl)) then x else
 	error ("The variable "^(string_of_id x)^" is already declared") in
   let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in 
-  let t = refresh_universes (pf_type_of gl c) in
+  let t = pf_type_of gl c in
   let newcl = mkNamedLetIn id c t ccl in
   tclTHENLIST
     [ convert_concl_no_check newcl DEFAULTcast;
@@ -1254,7 +1253,7 @@ let letin_tac with_eq name c occs gl =
 let forward usetac ipat c gl =
   match usetac with
   | None -> 
-      let t = refresh_universes (pf_type_of gl c) in
+      let t = pf_type_of gl c in
       tclTHENFIRST (assert_as true ipat t) (exact_no_check c) gl
   | Some tac -> 
       tclTHENFIRST (assert_as true ipat c) tac gl
@@ -1784,10 +1783,7 @@ let abstract_args gl id =
 	  let argty = pf_type_of gl arg in
 	  let liftarg = lift (List.length ctx) arg in
 	  let liftargty = lift (List.length ctx) argty in
-	  let convertible = 
-	    Reductionops.is_conv ctxenv sigma
-	      (Termops.refresh_universes ty) (Termops.refresh_universes liftargty) 
-	  in
+	  let convertible = Reductionops.is_conv ctxenv sigma ty liftargty in
 	    match kind_of_term arg with
 	      | Var _ | Rel _ when convertible -> 
 		    (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, (Anonymous, liftarg, liftarg) :: finalargs, env)