Merge pull request #370 from ppedrot/detuplify-impargs

rocq-archive · Nov 16, 2023 · 307889d · 307889d
2 parents fd9d22d + 01282b4
commit 307889d
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 1 deletion.
diff --git a/serapi/serapi_protocol.ml b/serapi/serapi_protocol.ml
@@ -180,7 +180,7 @@ let _pp_explicitation = let open Constrexpr in function
 
 let pp_implicit : Impargs.implicit_status -> Pp.t = function
   | None              -> Pp.str "!"
-  | Some (_expl, _, _) -> Pp.str "!" (* pp_explicitation expl *)
+  | Some _ -> Pp.str "!" (* pp_explicitation expl *)
 
 (*
 let pp_richpp xml =

diff --git a/serlib/ser_impargs.ml b/serlib/ser_impargs.ml
@@ -50,6 +50,10 @@ type implicit_position =
   [%import: Impargs.implicit_position]
   [@@deriving sexp]
 
+type implicit_status_info =
+  [%import: Impargs.implicit_status_info]
+  [@@deriving sexp]
+
 type implicit_status =
   [%import: Impargs.implicit_status]
   [@@deriving sexp]