Merge branch 'v8.6'

2 files changed, 5 insertions, 13 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 47d433d79..ebdf804ba 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -332,9 +332,6 @@ let error_missing_arg s =
 let filter_opts = ref false
 let exitcode () = if !filter_opts then 2 else 0
 
-let verb_compat_ntn = ref false
-let no_compat_ntn = ref false
-
 let print_where = ref false
 let print_config = ref false
 let print_tags = ref false
@@ -558,7 +555,6 @@ let parse_args arglist =
     |"-just-parsing" -> Vernac.just_parsing := true
     |"-m"|"--memory" -> memory_stat := true
     |"-noinit"|"-nois" -> load_init := false
-    |"-no-compat-notations" -> no_compat_ntn := true
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
     |"-native-compiler" ->
       if Coq_config.no_native_compiler then
@@ -576,7 +572,6 @@ let parse_args arglist =
     |"-unicode" -> add_require "Utf8_core"
     |"-v"|"--version" -> Usage.version (exitcode ())
     |"--print-version" -> Usage.machine_readable_version (exitcode ())
-    |"-verbose-compat-notations" -> verb_compat_ntn := true
     |"-where" -> print_where := true
     |"-xml" -> Flags.xml_export := true
 
@@ -637,9 +632,6 @@ let init_toplevel arglist =
       inputstate ();
       Mltop.init_known_plugins ();
       engage ();
-      (* Be careful to set these variables after the inputstate *)
-      Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
-(*       Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *)
       if (not !batch_mode || List.is_empty !compile_list)
          && Global.env_is_initial ()
       then Option.iter Declaremods.start_library !toplevel_name;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9415ade28..607bb6cfb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -576,18 +576,18 @@ let vernac_inductive poly lo finite indl =
   | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] ->
       CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead."
   | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] ->
-      vernac_record (match b with Class true -> Class false | _ -> b)
+      vernac_record (match b with Class _ -> Class false | _ -> b)
        poly finite id bl c oc fs
-  | [ ( id , bl , c , Class true, Constructors [l]), _ ] ->
+  | [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
       let f =
 	let (coe, ((loc, id), ce)) = l in
 	let coe' = if coe then Some true else None in
   	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) poly finite id bl c None [f]
-  | [ ( id , bl , c , Class true, _), _ ] ->
-      CErrors.error "Definitional classes must have a single method"
-  | [ ( id , bl , c , Class false, Constructors _), _ ] ->
+  | [ ( _ , _, _, Class _, Constructors _), [] ] ->
       CErrors.error "Inductive classes not supported"
+  | [ ( id , bl , c , Class _, _), _ :: _ ] ->
+      CErrors.error "where clause not supported for classes"
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
       CErrors.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function