diff options
| -rw-r--r-- | kernel/univ.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 18 | ||||
| -rw-r--r-- | pretyping/typing.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 12 |
4 files changed, 19 insertions, 18 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index a127fd5c0..dd00a5428 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -79,7 +79,7 @@ let super = function | Atom u -> Max ([],[u]) | Max _ -> - anomaly ("Cannot take the successor of a non variable universes:\n"^ + anomaly ("Cannot take the successor of a non variable universe:\n"^ "(maybe a bugged tactic)") (* Returns the formal universe that is greater than the universes u and v. diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 5cc146036..635a579c0 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 346942f1e..32df490db 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 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) |