Merge PR #6515: [api] Move `Vernacexpr` to parsing.

3 files changed, 10 insertions, 10 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3d627d2f6e..3c7ede3c99 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -334,8 +334,8 @@ let universe_proof_terminator compute_guard hook =
       Feedback.feedback Feedback.AddedAxiom
   | Proved (opaque,idopt,proof) ->
       let is_opaque, export_seff = match opaque with
-        | Vernacexpr.Transparent -> false, true
-        | Vernacexpr.Opaque      -> true, false
+        | Transparent -> false, true
+        | Opaque      -> true, false
       in
       let proof = get_proof proof compute_guard
         (hook (Some (proof.Proof_global.universes))) is_opaque in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1e7721f8fe..3bf0ca0a87 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -849,12 +849,12 @@ let obligation_terminator name num guard hook auto pf =
     let obl = obls.(num) in
     let status =
       match obl.obl_status, opq with
-      | (_, Evar_kinds.Expand), Vernacexpr.Opaque -> err_not_transp ()
-      | (true, _), Vernacexpr.Opaque -> err_not_transp ()
-      | (false, _), Vernacexpr.Opaque -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), Vernacexpr.Transparent ->
+      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
+      | (true, _), Opaque -> err_not_transp ()
+      | (false, _), Opaque -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), Transparent ->
         Evar_kinds.Define false
-      | (_, status), Vernacexpr.Transparent -> status
+      | (_, status), Transparent -> status
     in
     let obl = { obl with obl_status = false, status } in
     let ctx =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index eae8167c41..e1ce4e194c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -518,7 +518,7 @@ let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
   let status = Pfedit.by (Tactics.exact_proof c) in
-  save_proof (Vernacexpr.(Proved(Opaque,None)));
+  save_proof (Vernacexpr.(Proved(Proof_global.Opaque,None)));
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
@@ -855,7 +855,7 @@ let vernac_identity_coercion ~atts id qids qidt =
 
 let vernac_instance ~atts abst sup inst props pri =
   let global = not (make_section_locality atts.locality) in
-  Dumpglob.dump_constraint inst false "inst";
+  Dumpglob.dump_constraint (fst (pi1 inst)) false "inst";
   let program_mode = Flags.is_program_mode () in
   ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
 
@@ -1268,7 +1268,7 @@ let vernac_reserve bl =
 
 let vernac_generalizable ~atts =
   let local = make_non_locality atts.locality in
-  Implicit_quantifiers.declare_generalizable local
+  Implicit_quantifiers.declare_generalizable ~local
 
 let _ =
   declare_bool_option