[vernac] Cleanup on interface of Vernacentries

5 files changed, 70 insertions, 74 deletions

diff --git a/ide/idetop.ml b/ide/idetop.ml
index c38b8fa820..c6a8fdaa55 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -429,6 +429,11 @@ let quit = ref false
 (** Disabled *)
 let print_ast id = Xml_datatype.PCData "ERROR"
 
+let idetop_make_cases iname =
+  let qualified_iname = Libnames.qualid_of_string iname in
+  let iref = Nametab.global_inductive qualified_iname in
+  ComInductive.make_cases iref
+
 (** Grouping all call handlers together + error handling *)
 let eval_call c =
   let interruptible f x =
@@ -449,7 +454,7 @@ let eval_call c =
     Interface.search = interruptible search;
     Interface.get_options = interruptible get_options;
     Interface.set_options = interruptible set_options;
-    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.mkcases = interruptible idetop_make_cases;
     Interface.quit = (fun () -> quit := true);
     Interface.init = interruptible init;
     Interface.about = interruptible about;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index f530dad4fd..283e5ff50a 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -577,3 +577,43 @@ let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite =
   List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
+
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
+
+(*
+
+  HH notes in PR #679:
+
+  The Show Match could also be made more robust, for instance in the
+  presence of let in the branch of a constructor. A
+  decompose_prod_assum would probably suffice for that, but then, it
+  is a Context.Rel.Declaration.t which needs to be matched and not
+  just a pair (name,type).
+
+  Otherwise, this is OK. After all, the API on inductive types is not
+  so canonical in general, and in this simple case, working at the
+  low-level of mind_nf_lc seems reasonable (compared to working at the
+  higher-level of Inductiveops).
+
+*)
+
+let make_cases ind =
+  let open Declarations in
+  let mib, mip = Global.lookup_inductive ind in
+  Util.Array.fold_right_i
+    (fun i (ctx, _) l ->
+       let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
+       let rec rename avoid = function
+         | [] -> []
+         | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
+         | RelDecl.LocalAssum (n, _)::l ->
+           let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
+           Id.to_string n' :: rename (Id.Set.add n' avoid) l in
+       let al' = rename Id.Set.empty al in
+       let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
+       (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
+    mip.mind_nf_lc []
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index a77cd66a33..2d4cd7cac2 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -77,3 +77,11 @@ val interp_mutual_inductive :
   decl_notation list -> cumulative_inductive_flag ->
   poly:bool -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
+
+(** Prepare a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables.
+    [Not_found] is raised if the given string isn't the qualid of
+    a known inductive type. *)
+
+val make_cases : Names.inductive -> string list list
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e0183b941e..d02b703d6b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -31,7 +31,6 @@ open Lemmas
 open Locality
 open Attributes
 
-module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
 (** TODO: make this function independent of Ltac *)
@@ -146,59 +145,11 @@ let show_intro ~proof all =
     else mt ()
   end else mt ()
 
-(** Prepare a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables.
-    [Not_found] is raised if the given string isn't the qualid of
-    a known inductive type. *)
-
-(*
-
-  HH notes in PR #679:
-
-  The Show Match could also be made more robust, for instance in the
-  presence of let in the branch of a constructor. A
-  decompose_prod_assum would probably suffice for that, but then, it
-  is a Context.Rel.Declaration.t which needs to be matched and not
-  just a pair (name,type).
-
-  Otherwise, this is OK. After all, the API on inductive types is not
-  so canonical in general, and in this simple case, working at the
-  low-level of mind_nf_lc seems reasonable (compared to working at the
-  higher-level of Inductiveops).
-
-*)
-    
-let make_cases_aux glob_ref =
-  let open Declarations in
-  match glob_ref with
-    | Globnames.IndRef ind ->
-      let mib, mip = Global.lookup_inductive ind in
-	Util.Array.fold_right_i
-          (fun i (ctx, _) l ->
-             let al = Util.List.skipn (List.length mib.mind_params_ctxt) (List.rev ctx) in
-	     let rec rename avoid = function
-	       | [] -> []
-               | RelDecl.LocalDef _ :: l -> "_" :: rename avoid l
-               | RelDecl.LocalAssum (n, _)::l ->
-                   let n' = Namegen.next_name_away_with_default (Id.to_string Namegen.default_dependent_ident) n.Context.binder_name avoid in
-                   Id.to_string n' :: rename (Id.Set.add n' avoid) l in
-	     let al' = rename Id.Set.empty al in
-	     let consref = ConstructRef (ith_constructor_of_inductive ind (i + 1)) in
-	     (Libnames.string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty consref) :: al') :: l)
-          mip.mind_nf_lc []
-    | _ -> raise Not_found
-
-let make_cases s =
-  let qualified_name = Libnames.qualid_of_string s in
-  let glob_ref = Nametab.locate qualified_name in
-  make_cases_aux glob_ref
-
 (** Textual display of a generic "match" template *)
 
 let show_match id =
   let patterns =
-    try make_cases_aux (Nametab.global id)
+    try ComInductive.make_cases (Nametab.global_inductive id)
     with Not_found -> user_err Pp.(str "Unknown inductive type.")
   in
   let pr_branch l =
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 3563e9984a..e618cdcefe 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -8,17 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit
-
-(** Default proof mode set by `start_proof` *)
-val get_default_proof_mode : unit -> Pvernac.proof_mode
-
-val proof_mode_opt_name : string list
-
-(** Vernacular entries *)
-val vernac_require :
-  Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
-
 (** The main interpretation function of vernacular expressions *)
 val interp : ?verbosely:bool -> st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
@@ -32,22 +21,25 @@ val interp_qed_delayed_proof
   -> Vernacexpr.proof_end
   -> Vernacstate.t
 
-(** Prepare a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables.
-    [Not_found] is raised if the given string isn't the qualid of
-    a known inductive type. *)
-
-val make_cases : string -> string list list
-
 (** [with_fail ~st f] runs [f ()] and expects it to fail, otherwise it fails. *)
 val with_fail : st:Vernacstate.t -> (unit -> 'a) -> unit
 
-val command_focus : unit Proof.focus_kind
+(** Flag set when the test-suite is called. Its only effect to display
+    verbose information for [Fail] *)
+val test_mode : bool ref
+
+(** Vernacular require command *)
+val vernac_require :
+  Libnames.qualid option -> bool option -> Libnames.qualid list -> unit
 
+(** Hook to dissappear when #8240 is fixed *)
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
-(* Flag set when the test-suite is called. Its only effect to display
-   verbose information for `Fail` *)
-val test_mode : bool ref
+(** Miscellaneous stuff *)
+val command_focus : unit Proof.focus_kind
+
+(** Default proof mode set by `start_proof` *)
+val get_default_proof_mode : unit -> Pvernac.proof_mode
+
+val proof_mode_opt_name : string list