From 3696238f8dd435426080ba7d1b40c8ceacacb6ee Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 19 Aug 2015 18:30:50 +0200
Subject: Documentation by giving a name to a large type.

---
 intf/vernacexpr.mli | 7 ++++---
 stm/lemmas.mli      | 3 +--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index b72577e1e0..bb0331fcc4 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -196,6 +196,9 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
+type proof_expr =
+  lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)
+
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
   | TacNonTerm of Loc.t * string * (Names.Id.t * string) option
@@ -303,9 +306,7 @@ type vernac_expr =
   (* Gallina *)
   | VernacDefinition of
       (locality option * definition_object_kind) * lident * definition_expr
-  | VernacStartTheoremProof of theorem_kind * 
-      (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
-        bool
+  | VernacStartTheoremProof of theorem_kind * proof_expr list * bool
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of (locality option * assumption_object_kind) *
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index a0ddd265cb..6556aa2297 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -32,8 +32,7 @@ val start_proof_univs : Id.t -> goal_kind -> Evd.evar_map -> ?sign:Environ.named
   ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> 
   (Proof_global.proof_universes option -> unit declaration_hook) -> unit
 
-val start_proof_com : goal_kind ->
-  (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list ->
+val start_proof_com : goal_kind -> Vernacexpr.proof_expr list ->
   unit declaration_hook -> unit
 
 val start_proof_with_initialization : 
-- 
cgit v1.2.3