diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-26 14:25:30 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-11 13:41:26 +0200 |
| commit | 81107b12644c78f204d0a46df520b8b2d8e72142 (patch) | |
| tree | 85b9575ade7ce2dffff6ee66a652706c82b34d2c /pretyping/typing.mli | |
| parent | c538b7fd555828d9fba9ea97503fac6c70377b76 (diff) | |
Deprecate Evarconv.e_conv,e_cumul
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 4905adf1f..2239dda5f 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -46,8 +46,8 @@ val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> (** Raise an error message if bodies have types not unifiable with the expected ones *) -val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map ref -> - Names.Name.t array -> types array -> unsafe_judgment array -> unit +val check_type_fixpoint : ?loc:Loc.t -> env -> evar_map -> + Names.Name.t array -> types array -> unsafe_judgment array -> evar_map val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment |