diff options
| author | Emilio Jesus Gallego Arias | 2020-02-11 23:21:09 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-11 23:21:09 +0100 |
| commit | 44c3458deb687814379f7d05b27487b0ff9f2d38 (patch) | |
| tree | 27187ccdeb7609120e9a76814cd0d369945afc85 /pretyping | |
| parent | cbf5e7e49cfa243b6eac808241894fc504d84e5f (diff) | |
| parent | e85a9c7010f48fb0b79496f426df996b4e3dbb2e (diff) | |
Merge PR #11509: Add changelog and fixes for #10202
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 6 |
2 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cb0c4868b5..2d98d48aa0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,7 @@ open Evarconv module NamedDecl = Context.Named.Declaration -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = UnknownIfTermOrType | IsType | OfType of types | WithoutTypeConstraint let (!!) env = GlobEnv.env env @@ -1290,7 +1290,7 @@ let ise_pretype_gen flags env sigma lvar kind c = in let env = GlobEnv.make ~hypnaming env sigma lvar in let sigma', c', c'_ty = match kind with - | WithoutTypeConstraint -> + | WithoutTypeConstraint | UnknownIfTermOrType -> let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in sigma, j.uj_val, j.uj_type | OfType exptyp -> diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 18e416596e..ee57f690a1 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -38,7 +38,11 @@ val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map -> val search_guard : ?loc:Loc.t -> env -> int list list -> Constr.rec_declaration -> int array -type typing_constraint = OfType of types | IsType | WithoutTypeConstraint +type typing_constraint = + | UnknownIfTermOrType (** E.g., unknown if manual implicit arguments allowed *) + | IsType (** Necessarily a type *) + | OfType of types (** A term of the expected type *) + | WithoutTypeConstraint (** A term of unknown expected type *) type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr |