diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 3 | ||||
| -rw-r--r-- | pretyping/typing.mli | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 737c9fa1b..560289d1e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2337,7 +2337,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in (* The tycon may be ill-typed after abstraction. *) let env' = push_rel_context (context_of_arsign sign) env in - ignore(Typing.sort_of env' !evdref pred); pred + ignore(Typing.sort_of env' evdref pred); pred with e when Errors.noncritical e -> let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in lift nar t diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 8f5a7e39a..d2fddabdc 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -277,8 +277,7 @@ let type_of env evd c = (* Sort of a type *) -let sort_of env evd c = - let evdref = ref evd in +let sort_of env evdref c = let j = execute env evdref c in let a = e_type_judgment env evdref j in a.utj_type diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 03e62e006..8700df52a 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -22,7 +22,7 @@ val type_of : env -> evar_map -> constr -> types val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types (** Typecheck a type and return its sort *) -val sort_of : env -> evar_map -> types -> sorts +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 |