diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-10 11:31:01 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-10 11:34:08 +0200 |
| commit | 43104a0b94e42fb78764b5d1365ca1e85a158508 (patch) | |
| tree | 68943411671327facf236b25c6cabd63b96f90d0 /pretyping/typing.mli | |
| parent | 7a037b8c1de11b18d47b01e5b0262090f32bfc40 (diff) | |
Fixing #5077 (failure on typing a fixpoint with evars in its type).
Typing.type_of was using conversion for types of fixpoints while it
could have used unification.
Diffstat (limited to 'pretyping/typing.mli')
| -rw-r--r-- | pretyping/typing.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/typing.mli b/pretyping/typing.mli index dafd75231..22cb7f3b9 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -39,3 +39,8 @@ val solve_evars : env -> evar_map ref -> constr -> constr (** (first constr is term to match, second is return predicate) *) val check_allowed_sort : env -> evar_map -> pinductive -> constr -> constr -> unit + +(** Raise an error message if bodies have types not unifiable with the + expected ones *) +val check_type_fixpoint : Loc.t -> env -> evar_map ref -> + Names.Name.t array -> types array -> unsafe_judgment array -> unit |