fmt

hacspec · Nov 17, 2024 · 20db88c · 20db88c
1 parent 49c7f7c
commit 20db88c
Show file tree

Hide file tree

Showing 18 changed files with 77 additions and 694 deletions.
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
@@ -651,15 +651,3 @@ let parent_impl (id : t) : t option =
 
 module DefaultViewAPI = MakeViewAPI (DefaultNamePolicy)
 include DefaultViewAPI
-
-let remove_impl old =
-  let new_parent = (parent (parent old)).def_id in
-  {
-    kind = Macro;
-    (* Field; *)
-    def_id =
-      {
-        new_parent with
-        path = new_parent.path @ [ List.last_exn old.def_id.path ];
-      };
-  }
diff --git a/engine/lib/concrete_ident/concrete_ident.mli b/engine/lib/concrete_ident/concrete_ident.mli
@@ -74,6 +74,3 @@ identifier points to an [Impl] block. *)
 val parent_impl : t -> t option
 (** Returns the identifier pointing to the parent `impl` block, if it
 exists. *)
-
-val remove_impl : t -> t
-(** Returns the parent *)
diff --git a/engine/texput.log b/engine/texput.log
diff --git a/examples/coverage/proofs/coq/extraction/Coverage.v b/examples/coverage/proofs/coq/extraction/Coverage.v
diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum.v
diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_enum_Test.v
diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_functions.v
diff --git a/examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v b/examples/coverage/proofs/coq/extraction/Coverage_Test_instance.v