Update snapshots

cryspen · Feb 22, 2024 · 47450a2 · 47450a2
1 parent 11a0551
commit 47450a2
Show file tree

Hide file tree

Showing 4 changed files with 19 additions and 19 deletions.
diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml
@@ -560,7 +560,7 @@ functor
                 ^ ";")
               impl_list
           in
-          let ty_str = ty_to_string_with_paren self_ty in
+          let ty_str = ty_to_string_without_paren self_ty in
           "#[global] Instance" ^ " " ^ ty_str ^ "_" ^ name
           ^ params_to_string_typed arguments
           ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":=" ^ " " ^ "{"

diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml
@@ -53,7 +53,6 @@ struct
         include Features.SUBTYPE.On.Construct_base
         include Features.SUBTYPE.On.Slice
         include Features.SUBTYPE.On.Macro
-
         include Features.SUBTYPE.On.Loop
         include Features.SUBTYPE.On.For_loop
         include Features.SUBTYPE.On.While_loop

diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap
@@ -33,7 +33,7 @@ Import List.ListNotations.
 Open Scope Z_scope.
 Open Scope bool_scope.
 
-Class t_Trait Self := {
+Class t_Trait (Self : Type) := {
 }.
 
 (*Not implemented yet? todo(item)*)
@@ -48,9 +48,9 @@ Definition main_a_c (_ : unit) : unit :=
   tt.
 
 Definition main_a (x : T) : unit :=
-  let _ := (main_a_a tt) : unit in
-  let _ := (main_a_b tt) : unit in
-  let _ := (main_a_c tt) : unit in
+  let _ := main_a_a tt : unit in
+  let _ := main_a_b tt : unit in
+  let _ := main_a_c tt : unit in
   tt.
 
 Definition main_b_a (_ : unit) : unit :=
@@ -63,9 +63,9 @@ Definition main_b_c (_ : unit) : unit :=
   tt.
 
 Definition main_b (_ : unit) : unit :=
-  let _ := (main_b_a tt) : unit in
-  let _ := (main_b_b tt) : unit in
-  let _ := (main_b_c tt) : unit in
+  let _ := main_b_a tt : unit in
+  let _ := main_b_b tt : unit in
+  let _ := main_b_c tt : unit in
   tt.
 
 Definition main_c_a (_ : unit) : unit :=
@@ -78,20 +78,20 @@ Definition main_c_c (_ : unit) : unit :=
   tt.
 
 Definition main_c (_ : unit) : unit :=
-  let _ := (main_c_a tt) : unit in
-  let _ := (main_c_b tt) : unit in
-  let _ := (main_c_c tt) : unit in
+  let _ := main_c_a tt : unit in
+  let _ := main_c_b tt : unit in
+  let _ := main_c_c tt : unit in
   tt.
 
-Record t_Foo : Type :={
+Record t_Foo : Type := {
 }.
 
-Instance t_Foo_t_t_Trait : t_Trait t_Foo_t := {
+#[global] Instance t_Foo_t_t_Trait : t_Trait t_Foo_t := {
 }.
 
 Definition main (_ : unit) : unit :=
-  let _ := (main_a Foot_Foo_t) : unit in
-  let _ := (main_b tt) : unit in
-  let _ := (main_c tt) : unit in
+  let _ := main_a Foot_Foo_t : unit in
+  let _ := main_b tt : unit in
+  let _ := main_c tt : unit in
   tt.
 '''
diff --git a/test-harness/src/snapshots/toolchain__naming into-coq.snap b/test-harness/src/snapshots/toolchain__naming into-coq.snap
@@ -17,6 +17,7 @@ info:
     snapshot:
       stderr: false
       stdout: true
+    include_flag: ~
 ---
 exit = 0
 
@@ -53,7 +54,7 @@ Class t_T1 (Self : Type) := {
 #[global] Instance t_Foo_t_t_T1 : t_T1 t_Foo_t := {
 }.
 
-#[global] Instance (t_Foo_t × int8)_t_T1 : t_T1 (t_Foo_t × int8) := {
+#[global] Instance t_Foo_t × int8_t_T1 : t_T1 (t_Foo_t × int8) := {
 }.
 
 Class t_T2_for_a (Self : Type) := {
@@ -94,7 +95,7 @@ Record t_Arity1 (T : _) : Type := {
   0 : T;
 }.
 
-#[global] Instance t_Arity1_t ((t_Foo_t × int8))_t_T2_for_a : t_T2_for_a t_Arity1_t ((t_Foo_t × int8)) := {
+#[global] Instance t_Arity1_t (t_Foo_t × int8)_t_T2_for_a : t_T2_for_a (t_Arity1_t (t_Foo_t × int8)) := {
 }.
 
 Record t_B : Type := {