From ac594661da831e91f8c5a1b118ce13b90a7ec85f Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 15 Mar 2008 09:50:23 +0000 Subject: 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. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10674 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) (limited to 'tactics/tactics.ml') 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) -- cgit v1.2.3