Exposed the tp_nothing typolicy of EcTyping, so external tools can

check types, forbidding type variables.
EasyCrypt · Jan 14, 2025 · bba5194 · bba5194
1 parent e335db0
commit bba5194
Showing 1 changed file with 3 additions and 2 deletions.
diff --git 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: