From 2952ce43cdeb4f9d66732d54b0f8c9a47653512a Mon Sep 17 00:00:00 2001
From: Alley Stoughton <alley.stoughton@icloud.com>
Date: Tue, 14 Jan 2025 10:34:18 -0500
Subject: [PATCH] Exposed the tp_nothing typolicy of EcTyping, so external
 tools can check types, forbidding type variables.

---
 src/ecTyping.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/ecTyping.mli b/src/ecTyping.mli
index a09265998..7471c8d78 100644
--- a/src/ecTyping.mli
+++ b/src/ecTyping.mli
@@ -188,8 +188,9 @@ val unify_or_fail : env -> EcUnify.unienv -> EcLocation.t -> expct:ty -> ty -> u
 (* -------------------------------------------------------------------- *)
 type typolicy
 
-val tp_tydecl : typolicy
-val tp_relax  : typolicy
+val tp_tydecl  : typolicy
+val tp_relax   : typolicy
+val tp_nothing : typolicy
 
 (* -------------------------------------------------------------------- *)
 val transtyvars: