From 112827055097acaee8602c4bc75856196aeb8e1a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 28 Jun 2024 16:01:02 -0700 Subject: [PATCH 1/2] Env: ignoring env.lax for should_verify --- src/typechecker/FStar.TypeChecker.Env.fst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst index c430eca96f0..8cb7d415e5e 100644 --- a/src/typechecker/FStar.TypeChecker.Env.fst +++ b/src/typechecker/FStar.TypeChecker.Env.fst @@ -176,8 +176,7 @@ let missing_definition_list (e:env) : list lident = type sigtable = BU.smap sigelt let should_verify env = - not env.lax - && not env.admit + not env.admit && Options.should_verify (string_of_lid env.curmodule) let visible_at d q = match d, q with From e7da76f64efb4aa1f7d06031fcb320a67a2354aa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Fri, 28 Jun 2024 16:01:10 -0700 Subject: [PATCH 2/2] snap --- ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml index b78a5504583..0b093080d64 100644 --- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml @@ -1994,7 +1994,7 @@ type env_t = env type sigtable = FStar_Syntax_Syntax.sigelt FStar_Compiler_Util.smap let (should_verify : env -> Prims.bool) = fun env1 -> - ((Prims.op_Negation env1.lax) && (Prims.op_Negation env1.admit)) && + (Prims.op_Negation env1.admit) && (let uu___ = FStar_Ident.string_of_lid env1.curmodule in FStar_Options.should_verify uu___) let (visible_at : delta_level -> FStar_Syntax_Syntax.qualifier -> Prims.bool)