From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- pretyping/typing.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'pretyping/typing.ml') diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c6209cc3..fb5927db 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -270,7 +270,7 @@ let check env evdref c t = (* Type of a constr *) -let type_of env evd c = +let unsafe_type_of env evd c = let j = execute env (ref evd) c in j.uj_type @@ -283,7 +283,7 @@ let sort_of env evdref c = (* Try to solve the existential variables by typing *) -let e_type_of ?(refresh=false) env evd c = +let type_of ?(refresh=false) env evd c = let evdref = ref evd in let j = execute env evdref c in (* side-effect on evdref *) @@ -291,6 +291,15 @@ let e_type_of ?(refresh=false) env evd c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type else !evdref, j.uj_type +let e_type_of ?(refresh=false) env evdref c = + let j = execute env evdref c in + (* side-effect on evdref *) + if refresh then + let evd, c = Evarsolve.refresh_universes ~onlyalg:true (Some false) env !evdref j.uj_type in + let () = evdref := evd in + c + else j.uj_type + let solve_evars env evdref c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) -- cgit v1.2.3