diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/typing.ml | 5 | ||||
| -rw-r--r-- | pretyping/typing.mli | 2 |
2 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d2fddabdca..1485b77015 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -263,11 +263,10 @@ and execute_recdef env evdref (names,lar,vdef) = and execute_array env evdref = Array.map (execute env evdref) -let check env evd c t = - let evdref = ref evd in +let check env evdref c t = let j = execute env evdref c in if not (Evarconv.e_cumul env evdref j.uj_type t) then - error_actual_type env j (nf_evar evd t) + error_actual_type env j (nf_evar !evdref t) (* Type of a constr *) diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 8700df52a8..1d651e0c1e 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -25,7 +25,7 @@ val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types val sort_of : env -> evar_map ref -> types -> sorts (** Typecheck a term has a given type (assuming the type is OK) *) -val check : env -> evar_map -> constr -> types -> unit +val check : env -> evar_map ref -> constr -> types -> unit (** Returns the instantiated type of a metavariable *) val meta_type : evar_map -> metavariable -> types |