diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-04-14 15:18:11 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:59:00 +0200 |
| commit | 3869ffab2021b076054280f5eb4226ecda8caf75 (patch) | |
| tree | af6cae718a2b6e4acf72794cbe6677d253ede62f /pretyping/evarconv.mli | |
| parent | d2f36624980cdc169d0ebcc4c0be66446b4a8936 (diff) | |
- Add back some compatibility functions to avoid rewriting plugins.
- Fix in canonical structure inferce, we have to check that the heads
are convertible and keep universe information around.
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index aa45b5ef1..500bb5430 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -43,7 +43,8 @@ val check_problems_are_solved : env -> evar_map -> unit (** Check if a canonical structure is applicable *) val check_conv_record : constr * types Stack.t -> constr * types Stack.t -> - Univ.universe_context_set * constr * constr * constr list * (constr Stack.t * constr Stack.t) * + Univ.universe_context_set * (constr * constr) + * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * types Stack.t) * (constr Stack.t * types Stack.t) * constr * (int * constr) |