diff options
| author | Hugo Herbelin | 2020-02-09 06:48:07 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-11 16:18:59 +0100 |
| commit | 18e0103e33b276a88000dde8fccc772af2ca67ea (patch) | |
| tree | 00a7188ec3805645d185780aef9a9726b647be24 /pretyping/pretyping.ml | |
| parent | cd5bb3c76e430392e4363dc7b4b5bbe0cafa466f (diff) | |
Reinforcing the role of type "typing_constraint".
WithoutTypeConstraint says it can be a term. In particular, if it has
manual implicit arguments, these will be allowed only in leading
lambdas. I.e. it can start with "fun {x}" but not with "forall {x}".
New constructor UnknownIfTermOrType allows to be both a term or a
type. In particular, if it allowed start both with "fun {x}" and
"forall {x}".
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 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 -> |