Merge branch 'v8.5'

3 files changed, 36 insertions, 10 deletions

diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f46b90111..04182cf23 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -241,11 +241,26 @@ let compile_files () =
 (** Options for proof general *)
 
 let set_emacs () =
+  if not (Option.is_empty !toploop) then
+    error "Flag -emacs is incompatible with a custom toplevel loop";
   Flags.print_emacs := true;
   Pp.make_pp_emacs ();
   Vernacentries.qed_display_script := false;
   color := `OFF
 
+(** Options for CoqIDE *)
+
+let set_ideslave () =
+  if !Flags.print_emacs then error "Flags -ideslave and -emacs are incompatible";
+  toploop := Some "coqidetop";
+  Flags.ide_slave := true
+
+(** Options for slaves *)
+
+let set_toploop name =
+  if !Flags.print_emacs then error "Flags -toploop and -emacs are incompatible";
+  toploop := Some name
+
 (** GC tweaking *)
 
 (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the
@@ -498,7 +513,7 @@ let parse_args arglist =
     |"-main-channel" -> Spawned.main_channel := get_host_port opt (next())
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
-    |"-toploop" -> toploop := Some (next ())
+    |"-toploop" -> set_toploop (next ())
     |"-w" -> set_warning (next ())
 
     (* Options with zero arg *)
@@ -519,7 +534,7 @@ let parse_args arglist =
     |"-emacs" -> set_emacs ()
     |"-filteropts" -> filter_opts := true
     |"-h"|"-H"|"-?"|"-help"|"--help" -> usage ()
-    |"-ideslave" -> toploop := Some "coqidetop"; Flags.ide_slave := true
+    |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
     |"-just-parsing" -> Vernac.just_parsing := true
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7c1f05cd3..a041ee620 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -848,7 +848,7 @@ let make_interpretation_vars recvars allvars =
     (sc, make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
 
 let check_rule_productivity l =
-  if List.for_all (function NonTerminal _ -> true | _ -> false) l then
+  if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
     error "A notation must include at least one symbol.";
   if (match l with SProdList _ :: _ -> true | _ -> false) then
     error "A recursive notation must start with at least one symbol."
@@ -866,8 +866,21 @@ let is_not_printable onlyparse noninjective = function
   else onlyparse
 
 let find_precedence lev etyps symbols =
-  match symbols with
-  | NonTerminal x :: _ ->
+  let first_symbol =
+    let rec aux = function
+      | Break _ :: t -> aux t
+      | h :: t -> h
+      | [] -> assert false (* rule is known to be productive *) in
+    aux symbols in
+  let last_is_terminal () =
+    let rec aux b = function
+      | Break _ :: t -> aux b t
+      | Terminal _ :: t -> aux true t
+      | _ :: t -> aux false t
+      | [] -> b in
+    aux false symbols in
+  match first_symbol with
+  | NonTerminal x ->
       (try match List.assoc x etyps with
 	| ETConstr _ ->
 	    error "The level of the leftmost non-terminal cannot be changed."
@@ -890,9 +903,7 @@ let find_precedence lev etyps symbols =
 	if Option.is_empty lev then
 	  error "A left-recursive notation must have an explicit level."
 	else [],Option.get lev)
-  | Terminal _ ::l when
-      (match List.last symbols with Terminal _ -> true |_ -> false)
-      ->
+  | Terminal _ when last_is_terminal () ->
       if Option.is_empty lev then
 	([msg_info,strbrk "Setting notation at level 0."], 0)
       else [],Option.get lev
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fb57e55ef..b40f61b15 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -466,8 +466,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
- 	  start_proof_and_print (local,p,DefinitionBody Definition)
-	    [Some (lid,pl), (bl,t,None)] no_hook
+	  start_proof_and_print (local,p,DefinitionBody k)
+	    [Some (lid,pl), (bl,t,None)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None