7 files changed, 11 insertions, 55 deletions
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 65db4401d9..664010c917 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -80,9 +80,6 @@ type structured_one_inductive_expr = {
   ind_lc : (Id.t * constr_expr) list
 }
 
-type structured_inductive_expr =
-  local_binder_expr list * structured_one_inductive_expr list
-
 let minductive_message = function
   | []  -> user_err Pp.(str "No inductive definition.")
   | [x] -> (Id.print x ++ str " is defined")
@@ -468,9 +465,6 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive ~template udecl (paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
-  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations ~cumulative ~poly ~private_ind finite
-
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
   List.equal local_binder_eq bl1 bl2
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 97f930c0a1..285be8cd51 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Entries
-open Libnames
 open Vernacexpr
 open Constrexpr
 
@@ -33,12 +32,20 @@ val do_mutual_inductive
   -> Declarations.recursivity_kind
   -> unit
 
+(** User-interface API *)
+
+(** 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
+
 (************************************************************************)
-(** Internal API  *)
+(** Internal API, exported for Record                                   *)
 (************************************************************************)
 
-(** Exported for Record and Funind *)
-
 (** Registering a mutual inductive definition together with its
    associated schemes *)
 
@@ -55,41 +62,3 @@ val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
    inductive under consideration. *)
-
-(** Exported for Funind *)
-
-(** Extracting the semantical components out of the raw syntax of mutual
-   inductive declarations *)
-
-type structured_one_inductive_expr = {
-  ind_name : Id.t;
-  ind_arity : constr_expr;
-  ind_lc : (Id.t * constr_expr) list
-}
-
-type structured_inductive_expr =
-  local_binder_expr list * structured_one_inductive_expr list
-
-val extract_mutual_inductive_declaration_components :
-  (one_inductive_expr * decl_notation list) list ->
-    structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
-
-(** Typing mutual inductive definitions *)
-val interp_mutual_inductive
-  :  template:bool option
-  -> universe_decl_expr option
-  -> structured_inductive_expr
-  -> decl_notation list
-  -> cumulative:bool
-  -> poly:bool
-  -> private_ind:bool
-  -> 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/g_vernac.mlg b/vernac/g_vernac.mlg
index 15f9e0328c..ad5d98669d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -1141,7 +1141,6 @@ GRAMMAR EXTEND Gram
       | IDENT "Reset"; id = identref -> { VernacResetName id }
       | IDENT "Back" -> { VernacBack 1 }
       | IDENT "Back"; n = natural -> { VernacBack n }
-      | IDENT "BackTo"; n = natural -> { VernacBackTo n }
 
 (* Tactic Debugger *)
       |	IDENT "Debug"; IDENT "On" ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e25118e0a8..0eb0b1b6f6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -669,8 +669,6 @@ let string_of_definition_object_kind = let open Decls in function
         return (
           if Int.equal i 1 then keyword "Back" else keyword "Back" ++ pr_intarg i
         )
-      | VernacBackTo i ->
-        return (keyword "BackTo" ++ pr_intarg i)
 
     (* State management *)
       | VernacWriteState s ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 6c048c7d83..9af8d8b67c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2298,7 +2298,6 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacResetName _
   | VernacResetInitial
   | VernacBack _
-  | VernacBackTo _
   | VernacAbort _ ->
     anomaly (str "type_vernac")
   (* Syntax *)
@@ -2630,7 +2629,6 @@ and interp_expr ?proof ~atts ~st c =
   | VernacResetName _  -> anomaly (str "VernacResetName not handled by Stm.")
   | VernacResetInitial -> anomaly (str "VernacResetInitial not handled by Stm.")
   | VernacBack _       -> anomaly (str "VernacBack not handled by Stm.")
-  | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm.")
 
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6f09d9a39b..0968632c2d 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -359,7 +359,6 @@ type nonrec vernac_expr =
   | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int
-  | VernacBackTo of int
 
   (* Commands *)
   | VernacCreateHintDb of string * bool
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 1dd8164ebc..747998c6cc 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -32,7 +32,6 @@ let rec has_Fail v = v |> CAst.with_val (function
 let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
-  | VernacBackTo _
   | VernacBack _ -> true
   | _ -> false