diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/evd.ml | 2 | ||||
| -rw-r--r-- | kernel/evd.mli | 2 | ||||
| -rw-r--r-- | kernel/instantiate.ml | 2 | ||||
| -rw-r--r-- | kernel/term.ml | 4 | ||||
| -rw-r--r-- | kernel/term.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 |
7 files changed, 11 insertions, 5 deletions
diff --git a/kernel/evd.ml b/kernel/evd.ml index b12e6e9930..b31f2f6b79 100644 --- a/kernel/evd.ml +++ b/kernel/evd.ml @@ -20,7 +20,7 @@ type evar_body = | Evar_defined of constr type 'a evar_info = { - evar_concl : typed_type; + evar_concl : constr; evar_env : unsafe_env; evar_body : evar_body; evar_info : 'a } diff --git a/kernel/evd.mli b/kernel/evd.mli index 036443f129..62378f921e 100644 --- a/kernel/evd.mli +++ b/kernel/evd.mli @@ -23,7 +23,7 @@ type evar_body = | Evar_defined of constr type 'a evar_info = { - evar_concl : typed_type; + evar_concl : constr; evar_env : unsafe_env; evar_body : evar_body; evar_info : 'a } diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 37ffa5ca12..f3634eac5b 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -82,7 +82,7 @@ let existential_type sigma c = let (n,args) = destEvar c in let info = Evd.map sigma n in let hyps = evar_hyps info in - instantiate_constr (ids_of_sign hyps) (body_of_type info.evar_concl) + instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args) let existential_value sigma c = diff --git a/kernel/term.ml b/kernel/term.ml index 72d6cfbd2e..f7b7b607fd 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -72,6 +72,10 @@ let body_of_type ty = ty.body let incast_type tty = DOP2 (Cast, tty.body, (DOP0 (Sort tty.typ))) +let outcast_type = function + DOP2 (Cast, b, DOP0 (Sort s)) -> {body=b; typ=s} + | _ -> anomaly "outcast_type: Not an in-casted type judgement" + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) diff --git a/kernel/term.mli b/kernel/term.mli index 5118d39c5d..194681154a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -62,6 +62,8 @@ val body_of_type : typed_type -> constr val incast_type : typed_type -> constr +val outcast_type : constr -> typed_type + (*s Functions for dealing with constr terms. The following functions are intended to simplify and to uniform the manipulation of terms. Some of these functions may be overlapped with diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f20c5d213a..d224b0209e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -181,7 +181,7 @@ let type_of_existential env sigma c = let hyps = get_globals (context evi.Evd.evar_env) in let id = id_of_string ("?" ^ string_of_int ev) in check_hyps id env sigma hyps; - instantiate_type (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) + instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) (* Case. *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 1e602e0397..ddf09ab348 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -32,7 +32,7 @@ val type_of_inductive : unsafe_env -> 'a evar_map -> constr -> typed_type val type_of_constructor : unsafe_env -> 'a evar_map -> constr -> constr -val type_of_existential : unsafe_env -> 'a evar_map -> constr -> typed_type +val type_of_existential : unsafe_env -> 'a evar_map -> constr -> constr val type_of_case : unsafe_env -> 'a evar_map -> unsafe_judgment -> unsafe_judgment |