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}".
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b1e12bd66e..38f9b57e45 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2339,7 +2339,7 @@ let extract_ids env =
 let scope_of_type_kind sigma = function
   | IsType -> Notation.current_type_scope_name ()
   | OfType typ -> compute_type_scope sigma typ
-  | WithoutTypeConstraint -> None
+  | WithoutTypeConstraint | UnknownIfTermOrType -> None
 
 let empty_ltac_sign = {
   ltac_vars = Id.Set.empty;
-- 
cgit v1.2.3