From 18e0103e33b276a88000dde8fccc772af2ca67ea Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 9 Feb 2020 06:48:07 +0100
Subject: 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}".
---
 pretyping/pretyping.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping/pretyping.ml')

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 ->
-- 
cgit v1.2.3