From 6060c63e75e12b3671019dfaabfb118b69fd2005 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 29 Aug 2020 18:51:04 +0200
Subject: Make the Elim.branch_args type opaque.

---
 tactics/elim.mli | 8 +-------
 1 file changed, 1 insertion(+), 7 deletions(-)

diff --git a/tactics/elim.mli b/tactics/elim.mli
index 921a942e72..d470309b4a 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -14,13 +14,7 @@ open Tactypes
 
 (** Eliminations tactics. *)
 
-type branch_args = private {
-  ity        : Constr.pinductive;  (** the type we were eliminating on *)
-  branchnum  : int;         (** the branch number *)
-  nassums    : int;         (** number of assumptions/letin to be introduced *)
-  branchsign : bool list;   (** the signature of the branch.
-                                true=assumption, false=let-in *)
-  branchnames : intro_patterns}
+type branch_args
 
 val case_then_using :
   or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) ->
-- 
cgit v1.2.3