Fix strange bug

cryspen · Feb 22, 2024 · acbfd88 · acbfd88
1 parent bbb6712
commit acbfd88
Show file tree

Hide file tree

Showing 4 changed files with 452 additions and 450 deletions.
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -196,7 +196,8 @@ struct
   let rec ppat (p : pat) : C.AST.pat =
     match p.p with
     | PWild -> C.AST.WildPat
-    | PAscription { typ; pat; _ } -> C.AST.AscriptionPat (ppat pat, pty p.span typ)
+    | PAscription { typ; pat; _ } ->
+        C.AST.AscriptionPat (ppat pat, pty p.span typ)
     | PBinding
         {
           mut = Immutable;
@@ -278,7 +279,7 @@ struct
         {
           f = { e = GlobalVar (`Projector (`TupleField _)); _ };
           args = [ _ ];
-          _
+          _;
         } ->
         __TODO_term__ span "app global vcar projector tuple"
     | App { f = { e = GlobalVar x; _ }; args; _ } when Map.mem operators x ->
@@ -323,7 +324,8 @@ struct
         C.AST.Match
           ( pexpr scrutinee,
             List.map
-              ~f:(fun { arm = { arm_pat; body; _ }; _ } -> (ppat arm_pat, pexpr body))
+              ~f:(fun { arm = { arm_pat; body; _ }; _ } ->
+                (ppat arm_pat, pexpr body))
               arms )
     | Ascription _ -> __TODO_term__ span "asciption"
     | Construct { constructor = `TupleCons 1; fields = [ (_, e) ]; _ } ->
@@ -657,7 +659,7 @@ let string_of_item (item : item) : string =
   in
   List.map ~f:C.decl_to_string @@ Print.pitem item |> String.concat ~sep:"\n"
 
-let string_of_items =
+let string_of_items : AST.item list -> string =
   List.map ~f:string_of_item >> List.map ~f:String.strip
   >> List.filter ~f:(String.is_empty >> not)
   >> String.concat ~sep:"\n\n"

diff --git a/engine/backends/coq/coq/dune b/engine/backends/coq/coq/dune
@@ -17,4 +17,4 @@
 (env
  (_
   (flags
-   (:standard -w +A))))
+   (:standard -w +A -w "-4-40-42-44-45-48"))))
diff --git a/engine/backends/coq/ssprove/dune b/engine/backends/coq/ssprove/dune
@@ -8,7 +8,6 @@
    ppx_sexp_conv
    ppx_compare
    ppx_hash
-   visitors.ppx
    ppx_deriving.show
    ppx_deriving.eq
    ppx_inline
@@ -18,4 +17,4 @@
 (env
  (_
   (flags
-   (:standard -w -A))))
+   (:standard -w +A -w "-4-40-42-44-45-48"))))
-Original file line number
+Diff line change
@@ Expand Up / @@ -17,4 +17,4 @@ @@
     (env
      (_
       (flags
-       (:standard -w +A))))
+       (:standard -w +A -w "-4-40-42-44-45-48"))))