5 files changed, 11 insertions, 16 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d9b19c1ae6..4c24f51b1e 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -58,15 +58,8 @@ let new_entry name =
 let toplevel_selector = new_entry "vernac:toplevel_selector"
 let tacdef_body = new_entry "tactic:tacdef_body"
 
-(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for
-    proof editing and changes nothing else). Then sets it as the default proof mode. *)
-let _ =
-  let mode = {
-    Proof_global.name = "Classic";
-    set = (fun () -> Pvernac.set_command_entry tactic_mode);
-    reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
-  } in
-  Proof_global.register_proof_mode mode
+(* Registers [tactic_mode] as a parser for proof editing *)
+let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
 
 (* Hack to parse "[ id" without dropping [ *)
 let test_bracket_ident =
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 1ea6ff84d4..cdee012a82 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -83,7 +83,7 @@ open Obligations
 let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
 let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
 
-let classify_obbl _ = Vernacextend.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater)
+let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
 
 }
 
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 31fb1c9abf..db8d1b20d8 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -285,13 +285,13 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
            add_morphism_infer atts m n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts [] m s n;
        }
   | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
-    => { VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater }
+    => { VtStartProof(GuaranteesOpacity,[n]), VtLater }
     -> {
            add_morphism atts binders m s n;
        }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 46ea3819ac..7bf705ffeb 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -287,10 +287,10 @@ GRAMMAR EXTEND Gram
     [ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
   ;
   intropatterns:
-    [ [ l = LIST0 nonsimple_intropattern -> { l } ] ]
+    [ [ l = LIST0 intropattern -> { l } ] ]
   ;
   ne_intropatterns:
-    [ [ l = LIST1 nonsimple_intropattern -> { l } ] ]
+    [ [ l = LIST1 intropattern -> { l } ] ]
   ;
   or_and_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc }
@@ -317,7 +317,7 @@ GRAMMAR EXTEND Gram
       | "?" -> { IntroAnonymous }
       | id = ident -> { IntroIdentifier id } ] ]
   ;
-  nonsimple_intropattern:
+  intropattern:
     [ [ l = simple_intropattern -> { l }
       | "*"  -> { CAst.make ~loc @@ IntroForthcoming true }
       | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ]
@@ -534,6 +534,8 @@ GRAMMAR EXTEND Gram
           { TacAtom (CAst.make ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) }
       | IDENT "eintros"; pl = ne_intropatterns ->
           { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,pl)) }
+      | IDENT "eintros" ->
+          { TacAtom (CAst.make ~loc @@ TacIntroPattern (true,[CAst.make ~loc @@IntroForthcoming false])) }
 
       | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ",";
           inhyp = in_hyp_as -> { TacAtom (CAst.make ~loc @@ TacApply (true,false,cl,inhyp)) }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 4bb52f599a..2055b25ff4 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2014,7 +2014,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   ignore(new_instance ~program_mode:atts.program ~global:atts.global atts.polymorphic binders instance
-           (Some (true, CAst.make @@ CRecord []))
+     None
     ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)