From 0dcc1e133fe29293217a485d454cfdca43e61dc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 14 Oct 2024 06:53:04 -0700 Subject: [PATCH] snap --- .../fstar-lib/generated/FStarC_Parser_AST_Util.ml | 2 ++ .../generated/FStarC_SMTEncoding_Solver_Cache.ml | 15 +++++++++------ 2 files changed, 11 insertions(+), 6 deletions(-) diff --git a/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml b/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml index 4ece69e79bd..2e021cd4abc 100644 --- a/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml +++ b/ocaml/fstar-lib/generated/FStarC_Parser_AST_Util.ml @@ -514,6 +514,8 @@ let (eq_pragma : fun t1 -> fun t2 -> match (t1, t2) with + | (FStarC_Parser_AST.ShowOptions, FStarC_Parser_AST.ShowOptions) -> + true | (FStarC_Parser_AST.SetOptions s1, FStarC_Parser_AST.SetOptions s2) -> s1 = s2 | (FStarC_Parser_AST.ResetOptions s1, FStarC_Parser_AST.ResetOptions diff --git a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml index 89241361214..ef134ecf9a9 100644 --- a/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml +++ b/ocaml/fstar-lib/generated/FStarC_SMTEncoding_Solver_Cache.ml @@ -84,10 +84,13 @@ let (hashable_pragma : FStarC_Class_Hashable.hash = (fun uu___ -> match uu___ with + | FStarC_Syntax_Syntax.ShowOptions -> + FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int + Prims.int_one | FStarC_Syntax_Syntax.SetOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - Prims.int_one in + (Prims.of_int (2)) in let uu___2 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_string s in @@ -95,7 +98,7 @@ let (hashable_pragma : | FStarC_Syntax_Syntax.ResetOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (2)) in + (Prims.of_int (3)) in let uu___2 = FStarC_Class_Hashable.hash (FStarC_Class_Hashable.hashable_option @@ -104,7 +107,7 @@ let (hashable_pragma : | FStarC_Syntax_Syntax.PushOptions s -> let uu___1 = FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (3)) in + (Prims.of_int (4)) in let uu___2 = FStarC_Class_Hashable.hash (FStarC_Class_Hashable.hashable_option @@ -112,13 +115,13 @@ let (hashable_pragma : FStarC_Hash.mix uu___1 uu___2 | FStarC_Syntax_Syntax.PopOptions -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (4)) + (Prims.of_int (5)) | FStarC_Syntax_Syntax.RestartSolver -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (5)) + (Prims.of_int (6)) | FStarC_Syntax_Syntax.PrintEffectsGraph -> FStarC_Class_Hashable.hash FStarC_Class_Hashable.hashable_int - (Prims.of_int (6))) + (Prims.of_int (7))) } let rec (hash_sigelt : FStarC_Syntax_Syntax.sigelt -> FStarC_Hash.hash_code) = fun se -> hash_sigelt' se.FStarC_Syntax_Syntax.sigel