Merge branch 'master' of https://github.com/coq/coq

12 files changed, 88 insertions, 45 deletions

diff --git a/CHANGES b/CHANGES
index ca5172d7b7..fdf0c9d6be 100644
--- a/CHANGES
+++ b/CHANGES
@@ -133,6 +133,13 @@ Plugins
 - The mathematical proof language (also known as declarative mode) was removed.
 - A new command Extraction TestCompile has been introduced, not meant
   for the general user but instead for Coq's test-suite.
+- The extraction plugin is no longer loaded by default. It must be
+  explicitly loaded with [Require Extraction], which is backwards
+  compatible.
+- The functional induction plugin (which provides the [Function]
+  vernacular) is no longer loaded by default. It must be explicitly
+  loaded with [Require FunInd], which is backwards compatible.
+
 
 Dependencies
 
diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js
new file mode 100644
index 0000000000..371c5adc00
--- /dev/null
+++ b/dev/Coq_Bugzilla_autolink.user.js
@@ -0,0 +1,34 @@
+// ==UserScript==
+// @name        Coq Bugzilla autolink
+// @namespace   SkySkimmer
+// @include     https://github.com/coq/coq/*
+// @description Makes BZ#XXXX into links to bugzilla for GitHub
+// @version     1
+// @grant       none
+// ==/UserScript==
+
+var regex = /BZ#(\d+)/g;
+var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>';
+
+function doNode(node)
+{
+    node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("comment-body");
+
+for(var i=0; i<comments.length; i++)
+{
+    var pars = comments[i].getElementsByTagName("p");
+    for(var j=0; j<pars.length; j++)
+    {
+        doNode(pars[j]);
+    }
+}
+
+// usually 1 or 0 titles...
+var titles = document.getElementsByClassName("js-issue-title");
+for(var i=0; i<titles.length; i++)
+{
+    doNode(titles[i]);
+}
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 9be70e6d38..0dd08293c8 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -480,8 +480,11 @@ object(self)
       | Message(lvl, loc, msg), Some (id,sentence) ->
           log_pp ?id Pp.(str "Msg " ++ msg);
           messages#push lvl msg
+      (* We do nothing here as for BZ#5583 *)
+      | Message(Error, loc, msg), None ->
+          log_pp Pp.(str "Error Msg without a sentence" ++ msg)
       | Message(lvl, loc, msg), None ->
-          log_pp Pp.(str "Msg " ++ msg);
+          log_pp Pp.(str "Msg without a sentence " ++ msg);
           messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
@@ -655,7 +658,7 @@ object(self)
         with Doc.Empty -> initial_state | Invalid_argument _ -> assert false in
       loop tip [] in
     Coq.bind fill_queue process_queue
-  
+
   method join_document =
    let next = function
      | Good _ ->
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 13de731f54..970666638c 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -206,7 +206,7 @@ let rec find_project_file ~from ~projfile_name =
   if Sys.file_exists fname then Some fname
   else
     let newdir = Filename.dirname from in
-    if newdir = "" || newdir = "/" then None
+    if newdir = from then None
     else find_project_file ~from:newdir ~projfile_name
 ;;
 
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 870137ca11..d51b8b54e5 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -34,6 +34,7 @@ let default_levels =
   [200,Extend.RightA,false;
    100,Extend.RightA,false;
    99,Extend.RightA,true;
+   90,Extend.RightA,true;
    10,Extend.RightA,false;
    9,Extend.RightA,false;
    8,Extend.RightA,true;
@@ -44,6 +45,7 @@ let default_pattern_levels =
   [200,Extend.RightA,true;
    100,Extend.RightA,false;
    99,Extend.RightA,true;
+   90,Extend.RightA,true;
    11,Extend.LeftA,false;
    10,Extend.RightA,false;
    1,Extend.LeftA,false;
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 4e8b98fcf2..844c040fdf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -376,6 +376,7 @@ GEXTEND Gram
     | "100" RIGHTA
       [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> CAst.make ~loc:!@loc @@ CPatOr (p::pl) ]
     | "99" RIGHTA [ ]
+    | "90" RIGHTA [ ]
     | "11" LEFTA
       [ p = pattern; "as"; id = ident ->
         CAst.make ~loc:!@loc @@ CPatAlias (p, id) ]
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 2ea0f60ebc..86c983bdd9 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -388,16 +388,7 @@ let vernac_solve n info tcom b =
     p,status) in
     if not status then Feedback.feedback Feedback.AddedAxiom
 
-let pr_range_selector (i, j) =
-  if Int.equal i j then int i
-  else int i ++ str "-" ++ int j
-
-let pr_ltac_selector = function
-| SelectNth i -> int i ++ str ":"
-| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
-    str "]" ++ str ":"
-| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-| SelectAll -> str "all" ++ str ":"
+let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
 
 VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
 | [ toplevel_selector(s) ] -> [ s ]
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 8a0764975d..d8bd166208 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -477,12 +477,14 @@ type 'a extra_genarg_printer =
     if Int.equal i j then int i
     else int i ++ str "-" ++ int j
 
-  let pr_goal_selector = function
-    | SelectNth i -> int i ++ str ":"
-    | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
-        str "]" ++ str ":"
-    | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
-    | SelectAll -> str "all" ++ str ":"
+let pr_goal_selector toplevel = function
+  | SelectNth i -> int i ++ str ":"
+  | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
+  | SelectId id -> str "[" ++ Id.print id ++ str "]:"
+  | SelectAll -> assert toplevel; str "all:"
+
+let pr_goal_selector ~toplevel s =
+  (if toplevel then mt () else str "only ") ++ pr_goal_selector toplevel s
 
   let pr_lazy = function
     | General -> keyword "multi"
@@ -988,7 +990,7 @@ type 'a extra_genarg_printer =
               keyword "solve" ++ spc () ++ pr_seq_body (pr_tac ltop) tl, llet
             | TacComplete t ->
               pr_tac (lcomplete,E) t, lcomplete
-            | TacSelect (s, tac) -> pr_goal_selector s ++ spc () ++ pr_tac ltop tac, latom
+            | TacSelect (s, tac) -> pr_goal_selector ~toplevel:false s ++ spc () ++ pr_tac ltop tac, latom
             | TacId l ->
               keyword "idtac" ++ prlist (pr_arg (pr_message_token pr.pr_name)) l, latom
             | TacAtom (loc,t) ->
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 1f6ebaf448..c79d5b389f 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -53,6 +53,8 @@ type pp_tactic = {
   pptac_prods : grammar_terminals;
 }
 
+val pr_goal_selector : toplevel:bool -> goal_selector -> Pp.t
+
 val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit
 
 val pr_with_occurrences :
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 69a49749cd..f3e8e72bb7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -464,7 +464,7 @@ and detype_r d flags avoid env sigma t =
           (* Using a dash to be unparsable *)
 	  GEvar (Id.of_string_soft "CONTEXT-HOLE", [])
         else
-	  GEvar (Id.of_string_soft ("INTERNAL#" ^ string_of_int n), [])
+	  GEvar (Id.of_string_soft ("M" ^ string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (VarRef id, None)
 	 with Not_found -> GVar id)
diff --git a/stm/stm.ml b/stm/stm.ml
index 75ec946f03..7c44fc86fb 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2000,24 +2000,24 @@ let collect_proof keep cur hd brkind id =
    | { expr =  (VernacRequire _ | VernacImport _) } -> true
    | ast -> may_pierce_opaque ast in
  let parent = function Some (p, _) -> p | None -> assert false in
- let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
+ let is_empty = function `Async(_,[],_,_) | `MaybeASync(_,[],_,_) -> true | _ -> false in
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
     | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
-      when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
+      when too_complex_to_delegate x -> `Sync(no_name,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
     | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
-    | `Alias _ -> `Sync (no_name,None,`Alias)
+    | `Alias _ -> `Sync (no_name,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
-        `Sync (no_name,proof_using_ast last,`MutualProofs)
+        `Sync (no_name,`MutualProofs)
     | `Fork((_,_,Doesn'tGuaranteeOpacity,_), _) ->
-        `Sync (no_name,proof_using_ast last,`Doesn'tGuaranteeOpacity)
+        `Sync (no_name,`Doesn'tGuaranteeOpacity)
     | `Fork((_,hd',GuaranteesOpacity,ids), _) when has_proof_using last ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
-        `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+        `ASync (parent last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
        has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
        !Flags.compilation_mode = Flags.BuildVio ->
@@ -2026,31 +2026,32 @@ let collect_proof keep cur hd brkind id =
           let name, hint = name ids, get_hint_ctx loc  in
           let t, v = proof_no_using last in
           v.expr <- VernacProof(t, Some hint);
-          `ASync (parent last,proof_using_ast last,accn,name,delegate name)
+          `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
-          `MaybeASync (parent last, None, accn, name, delegate name))
+          `MaybeASync (parent last, accn, name, delegate name))
     | `Fork((_, hd', GuaranteesOpacity, ids), _) ->
         assert (VCS.Branch.equal hd hd' || VCS.Branch.equal hd VCS.edit_branch);
         let name = name ids in
-        `MaybeASync (parent last, None, accn, name, delegate name)
+        `MaybeASync (parent last, accn, name, delegate name)
     | `Sideff _ ->
        warn_deprecated_nested_proofs ();
-        `Sync (no_name,None,`NestedProof)
-    | _ -> `Sync (no_name,None,`Unknown) in
+        `Sync (no_name,`NestedProof)
+    | _ -> `Sync (no_name,`Unknown) in
  let make_sync why = function
-   | `Sync(name,pua,_) -> `Sync (name,pua,why)
-   | `MaybeASync(_,pua,_,name,_) -> `Sync (name,pua,why)
-   | `ASync(_,pua,_,name,_) -> `Sync (name,pua,why) in
+   | `Sync(name,_) -> `Sync (name,why)
+   | `MaybeASync(_,_,name,_) -> `Sync (name,why)
+   | `ASync(_,_,name,_) -> `Sync (name,why) in
+
  let check_policy rc = if async_policy () then rc else make_sync `Policy rc in
  match cur, (VCS.visit id).step, brkind with
  | (parent, { expr = VernacExactProof _ }), `Fork _, _
  | (parent, { expr = VernacTime (_, VernacExactProof _) }), `Fork _, _ ->
-     `Sync (no_name,None,`Immediate)
+     `Sync (no_name,`Immediate)
  | _, _, { VCS.kind = `Edit _ }  -> check_policy (collect (Some cur) [] id)
  | _ ->
-     if is_defined cur then `Sync (no_name,None,`Transparent)
-     else if keep == VtDrop then `Sync (no_name,None,`Aborted)
+     if is_defined cur then `Sync (no_name,`Transparent)
+     else if keep == VtDrop then `Sync (no_name,`Aborted)
      else
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
@@ -2222,7 +2223,7 @@ let known_state ?(redefine_qed=false) ~cache id =
           ), `Yes, true
       | `Qed ({ qast = x; keep; brinfo; brname } as qed, eop) ->
           let rec aux = function
-          | `ASync (block_start, pua, nodes, name, delegate) -> (fun () ->
+          | `ASync (block_start, nodes, name, delegate) -> (fun () ->
                 assert(keep == VtKeep || keep == VtKeepAsAxiom);
                 let drop_pt = keep == VtKeepAsAxiom in
                 let block_stop, exn_info, loc = eop, (id, eop), x.loc in
@@ -2269,10 +2270,10 @@ let known_state ?(redefine_qed=false) ~cache id =
                 end;
                 Proof_global.discard_all ()
               ), (if redefine_qed then `No else `Yes), true
-          | `Sync (name, _, `Immediate) -> (fun () -> 
+          | `Sync (name, `Immediate) -> (fun () -> 
                 reach eop; stm_vernac_interp id x; Proof_global.discard_all ()
               ), `Yes, true
-          | `Sync (name, pua, reason) -> (fun () ->
+          | `Sync (name, reason) -> (fun () ->
                 log_processing_sync id name reason;
                 reach eop;
                 let wall_clock = Unix.gettimeofday () in
@@ -2297,12 +2298,12 @@ let known_state ?(redefine_qed=false) ~cache id =
                   (Printf.sprintf "%.3f" (wall_clock3 -. wall_clock2));
                 Proof_global.discard_all ()
               ), `Yes, true
-          | `MaybeASync (start, pua, nodes, name, delegate) -> (fun () ->
+          | `MaybeASync (start, nodes, name, delegate) -> (fun () ->
                 reach ~cache:`Shallow start;
                 (* no sections *)
                 if CList.is_empty (Environ.named_context (Global.env ()))
-                then Util.pi1 (aux (`ASync (start, pua, nodes, name, delegate))) ()
-                else Util.pi1 (aux (`Sync (name, pua, `NoPU_NoHint_NoES))) ()
+                then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) ()
+                else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) ()
               ), (if redefine_qed then `No else `Yes), true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index a0b6bfbbed..6ddeeb9b28 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -94,7 +94,7 @@ let rcs = "\036" rcs_keyword [^ '$']* "\036"
 let stars = "(*" '*'* "*)"
 let dot = '.' (' ' | '\t' | '\n' | '\r' | eof)
 let proof_start =
-  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" | "Next"
+  "Theorem" | "Lemma" | "Fact" | "Remark" | "Goal" | "Correctness" | "Obligation" space+ (['0' - '9'])+ | "Next" space+ "Obligation"
 let def_start =
   "Definition" | "Fixpoint" | "Instance"
 let proof_end =