VernacDeclareInstances -> VernacExistingInstance

5 files changed, 7 insertions, 7 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 454a4b66e7..b9cc7e5916 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -160,7 +160,7 @@ let classify_vernac e =
     | VernacMemOption _ | VernacPrintOption _
     | VernacGlobalCheck _
     | VernacDeclareReduction _
-    | VernacDeclareClass _ | VernacDeclareInstances _
+    | VernacDeclareClass _ | VernacExistingInstance _
     | VernacRegister _
     | VernacNameSectionHypSet _
     | VernacDeclareCustomEntry _
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 22528a607f..b5bc1c8111 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -687,13 +687,13 @@ GRAMMAR EXTEND Gram
 
       | IDENT "Existing"; IDENT "Instance"; id = global;
           info = hint_info ->
-	  { VernacDeclareInstances [id, info] }
+	  { VernacExistingInstance [id, info] }
 
       | IDENT "Existing"; IDENT "Instances"; ids = LIST1 global;
         pri = OPT [ "|"; i = natural -> { i } ] ->
          { let info = { Typeclasses.hint_priority = pri; hint_pattern = None } in
          let insts = List.map (fun i -> (i, info)) ids in
-	  VernacDeclareInstances insts }
+	  VernacExistingInstance insts }
 
       | IDENT "Existing"; IDENT "Class"; is = global -> { VernacDeclareClass is }
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e0dd3380f9..8be43c9495 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -912,7 +912,7 @@ open Pputils
             keyword "Context" ++ pr_and_type_binders_arg l)
         )
 
-      | VernacDeclareInstances insts ->
+      | VernacExistingInstance insts ->
          let pr_inst (id, info) =
            pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info
          in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dbccea1117..28ce619f10 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1016,7 +1016,7 @@ let vernac_instance ~atts abst sup inst props pri =
 let vernac_context ~poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_declare_instances ~section_local insts =
+let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
   List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
 
@@ -2230,7 +2230,7 @@ let interp ?proof ~atts ~st c =
   | VernacInstance (abst, sup, inst, props, info) ->
       vernac_instance ~atts abst sup inst props info
   | VernacContext sup -> vernac_context ~poly:(only_polymorphism atts) sup
-  | VernacDeclareInstances insts -> with_section_locality ~atts vernac_declare_instances insts
+  | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts
   | VernacDeclareClass id -> unsupported_attributes atts; vernac_declare_class id
 
   (* Solving *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 417c9ebfbd..9b36159073 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -308,7 +308,7 @@ type nonrec vernac_expr =
 
   | VernacContext of local_binder_expr list
 
-  | VernacDeclareInstances of
+  | VernacExistingInstance of
     (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacDeclareClass of qualid (* inductive or definition name *)