summaryrefslogtreecommitdiff
path: root/pretyping/retyping.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /pretyping/retyping.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'pretyping/retyping.ml')
-rw-r--r--pretyping/retyping.ml27
1 files changed, 13 insertions, 14 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 19e46a47..1e0649da 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: retyping.ml 11897 2009-02-09 19:28:02Z barras $ *)
+(* $Id$ *)
open Util
open Term
@@ -44,11 +44,11 @@ let type_of_var env id =
with Not_found ->
anomaly ("type_of: variable "^(string_of_id id)^" unbound")
-let retype sigma metamap =
+let retype sigma =
let rec type_of env cstr=
match kind_of_term cstr with
| Meta n ->
- (try strip_outer_cast (List.assoc n metamap)
+ (try strip_outer_cast (Evd.meta_ftype sigma n).Evd.rebus
with Not_found -> anomaly ("type_of: unknown meta " ^ string_of_int n))
| Rel n ->
let (_,_,ty) = lookup_rel n env in
@@ -81,7 +81,7 @@ let retype sigma metamap =
| Cast (c,_, t) -> t
| Sort _ | Prod _ -> mkSort (sort_of env cstr)
- and sort_of env t =
+ and sort_of env t =
match kind_of_term t with
| Cast (c,_, s) when isSort s -> destSort s
| Sort (Prop c) -> type1_sort
@@ -111,14 +111,14 @@ let retype sigma metamap =
| Cast (c,_, s) when isSort s -> family_of_sort (destSort s)
| Sort (Prop c) -> InType
| Sort (Type u) -> InType
- | Prod (name,t,c2) ->
+ | Prod (name,t,c2) ->
let s2 = sort_family_of (push_rel (name,None,t) env) c2 in
if Environ.engagement env <> Some ImpredicativeSet &&
s2 = InSet & sort_family_of env t = InType then InType else s2
| App(f,args) when isGlobalRef f ->
let t = type_of_global_reference_knowing_parameters env f args in
family_of_sort (sort_of_atomic_type env sigma t args)
- | App(f,args) ->
+ | App(f,args) ->
family_of_sort (sort_of_atomic_type env sigma (type_of env f) args)
| Lambda _ | Fix _ | Construct _ ->
anomaly "sort_of: Not a type (1)"
@@ -140,10 +140,10 @@ let retype sigma metamap =
in type_of, sort_of, sort_family_of,
type_of_global_reference_knowing_parameters
-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 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 = retype sigma [] in f env c args
+ let _,_,_,f = retype sigma in f env c args
let type_of_global_reference_knowing_conclusion env sigma c conclty =
let conclty = nf_evar sigma conclty in
@@ -161,11 +161,10 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
(* 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)
+let get_type_of ?(refresh=true) env sigma c =
+ let f,_,_,_ = retype sigma in
+ let t = f env c in
+ if refresh then refresh_universes t else t
(* Makes an assumption from a constr *)
let get_assumption_of env evc c = c