diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 11 | ||||
| -rw-r--r-- | pretyping/typing.mli | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ebd099fa3..7f84828f1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -45,6 +45,11 @@ let e_judge_of_apply env evdref funj argjv = apply_rec (n+1) (subst1 hj.uj_val c2) restjl else error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv + | Evar ev -> + let (evd',t) = Evarutil.define_evar_as_product !evdref ev in + evdref := evd'; + let (_,_,c2) = destProd t in + apply_rec (n+1) (subst1 hj.uj_val c2) restjl | _ -> error_cant_apply_not_functional env funj argjv in @@ -261,6 +266,12 @@ let sort_of env evd c = (* Try to solve the existential variables by typing *) +let e_type_of env evd c = + let evdref = ref evd in + let j = execute env evdref c in + (* side-effect on evdref *) + !evdref, Termops.refresh_universes j.uj_type + let solve_evars env evd c = let evdref = ref evd in let c = (execute env evdref c).uj_val in diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 2c9a6c6c0..224fd995a 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -17,6 +17,9 @@ open Evd (** Typecheck a term and return its type *) val type_of : env -> evar_map -> constr -> types +(** Typecheck a term and return its type + updated evars *) +val e_type_of : env -> evar_map -> constr -> evar_map * types + (** Typecheck a type and return its sort *) val sort_of : env -> evar_map -> types -> sorts |