Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

9 files changed, 69 insertions, 48 deletions

diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index 15413d51..b7eb9b1f 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -12,8 +12,6 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
-open Locus
-open Genredexpr
 
 module type Pp = sig
 
diff --git a/printing/pptactic.mli b/printing/pptactic.mli
index 284237f0..fa91aefc 100644
--- a/printing/pptactic.mli
+++ b/printing/pptactic.mli
@@ -15,9 +15,7 @@ open Names
 open Constrexpr
 open Tacexpr
 open Ppextend
-open Environ
-open Pattern
-open Misctypes
+
 
 type 'a raw_extra_genarg_printer =
     (constr_expr -> std_ppcmds) ->
@@ -63,3 +61,4 @@ include Pptacticsig.Pp
     located in {!Ppannotation.t}. *)
 module Richpp : Pptacticsig.Pp
 
+val ltop : tolerability
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 98b5757d..166a6675 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -8,7 +8,6 @@
 
 open Pp
 open Genarg
-open Names
 open Constrexpr
 open Tacexpr
 open Ppextend
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e9e335ec..89ffae4b 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -740,9 +740,14 @@ module Make
 
         | VernacEndProof (Proved (opac,o)) -> return (
           match o with
-            | None -> if opac then keyword "Qed" else keyword "Defined"
+            | None -> (match opac with
+                | Transparent -> keyword "Defined"
+                | Opaque None -> keyword "Qed"
+                | Opaque (Some l) ->
+                    keyword "Qed" ++ spc() ++ str"export" ++
+                      prlist_with_sep (fun () -> str", ") pr_lident l)
             | Some (id,th) -> (match th with
-                | None -> (if opac then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
+                | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
                 | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
         )
         | VernacExactProof c ->
@@ -858,10 +863,14 @@ module Make
         | VernacNameSectionHypSet (id,set) ->
           return (hov 2 (keyword "Package" ++ spc() ++ pr_lident id ++ spc()++
           str ":="++spc()++pr_using set))
-        | VernacRequire (exp, l) ->
+        | VernacRequire (from, exp, l) ->
+          let from = match from with
+          | None -> mt ()
+          | Some r -> keyword "From" ++ spc () ++ pr_module r ++ spc ()
+          in
           return (
             hov 2
-              (keyword "Require" ++ spc() ++ pr_require_token exp ++
+              (from ++ keyword "Require" ++ spc() ++ pr_require_token exp ++
                  prlist_with_sep sep pr_module l)
           )
         | VernacImport (f,l) ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 223377c2..4a66c33d 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -109,7 +109,7 @@ let print_impargs_list prefix l =
 	 [(if ismt prefix then str "When" else prefix ++ str ", when") ++
 	   str " applied to " ++
 	   (if Int.equal n1 n2 then int_or_no n2 else
-	    if Int.equal n1 0 then str "less than " ++ int n2
+	    if Int.equal n1 0 then str "no more than " ++ int n2
 	    else int n1 ++ str " to " ++ int_or_no n2) ++
 	    str (String.plural n2 " argument") ++ str ":";
           v 0 (prlist_with_sep cut (fun x -> x)
@@ -197,11 +197,13 @@ let print_opacity ref =
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-    pr_global ref ++ str " is " ++ str 
+  if Flags.is_universe_polymorphism () || poly || template_poly then
+    [ pr_global ref ++ str " is " ++ str
       (if poly then "universe polymorphic"
        else if template_poly then
 	 "template universe polymorphic"
-       else "not universe polymorphic")
+       else "not universe polymorphic") ]
+  else []
 
 let print_primitive_record mipv = function
   | Some (Some (_, ps,_)) ->
@@ -214,9 +216,8 @@ let print_primitive ref =
     let mib,_ = Global.lookup_inductive ind in
       print_primitive_record mib.mind_packets mib.mind_record
   | _ -> []
-    
+
 let print_name_infos ref =
-  let poly = print_polymorphism ref in
   let impls = implicits_of_global ref in
   let scopes = Notation.find_arguments_scope ref in
   let renames =
@@ -228,7 +229,8 @@ let print_name_infos ref =
        print_ref true ref; blankline]
     else
       [] in
-  poly :: print_primitive ref @
+  print_polymorphism ref @
+  print_primitive ref @
   type_info_for_implicit @
   print_renames_list (mt()) renames @
   print_impargs_list (mt()) impls @
diff --git a/printing/printer.ml b/printing/printer.ml
index 3403fb9c..0d3a1c17 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -11,7 +11,6 @@ open Errors
 open Util
 open Names
 open Term
-open Vars
 open Environ
 open Globnames
 open Nametab
@@ -446,6 +445,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i
 
 let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
 
+(* Display a list of evars given by their name, with a prefix *)
+let pr_ne_evar_set hd tl sigma l =
+  if l != Evar.Set.empty then
+    let l = Evar.Set.fold (fun ev ->
+      Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev)))
+      l Evar.Map.empty in
+    hd ++ pr_evars sigma l ++ tl
+  else
+    mt ()
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
@@ -535,26 +544,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
     else 
       pr_rec 1 (g::l)
   in
+  (* Side effect! This has to be made more robust *)
+  let () =
+    match close_cmd with
+    | Some cmd -> msg_info cmd
+    | None -> ()
+  in
   match goals with
   | [] ->
       begin
-	match close_cmd with
-	  Some cmd ->
-	    (str "Subproof completed, now type " ++ str cmd ++
-	       str ".")
-	| None ->
-	    let exl = Evarutil.non_instantiated sigma in
-	    if Evar.Map.is_empty exl then
-	      (str"No more subgoals."
-	       ++ emacs_print_dependent_evars sigma seeds)
-	    else
-	      let pei = pr_evars_int sigma 1 exl in
-	      (str "No more subgoals but non-instantiated existential " ++
-		 str "variables:" ++ fnl () ++ (hov 0 pei)
-	       ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
-                 str "You can use Grab Existential Variables.")
+	let exl = Evarutil.non_instantiated sigma in
+	if Evar.Map.is_empty exl then
+	  (str"No more subgoals."
+	   ++ emacs_print_dependent_evars sigma seeds)
+	else
+	  let pei = pr_evars_int sigma 1 exl in
+	  (str "No more subgoals but non-instantiated existential " ++
+	   str "variables:" ++ fnl () ++ (hov 0 pei)
+	   ++ emacs_print_dependent_evars sigma seeds ++ fnl () ++
+           str "You can use Grab Existential Variables.")
       end
-  | [g] when not !Flags.print_emacs ->
+  | [g] when not !Flags.print_emacs && pr_first ->
       let pg = default_pr_goal { it = g ; sigma = sigma; } in
       v 0 (
 	str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra
@@ -563,8 +573,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
       )
   | g1::rest ->
       let goals = print_multiple_goals g1 rest in
+      let ngoals = List.length rest+1 in
       v 0 (
-	int(List.length rest+1) ++ focused_if_needed ++ str"subgoals" ++
+	int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++
           print_extra ++
           str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1")
         ++ pr_goal_tag g1
@@ -578,7 +589,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals
 
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 }
@@ -622,10 +633,14 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	    fnl ()
             ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf
 	  | _ , _, _ ->
-	    msg_info (str "This subproof is complete, but there are still unfocused goals." ++
-			(match Proof_global.Bullet.suggest p
-			 with None  -> str"" | Some s -> fnl () ++ str s));
-	    fnl () ++ pr_subgoals ~pr_first:false None bsigma seeds shelf [] bgoals
+            let end_cmd =
+              strbrk "This subproof is complete, but there are still \
+              unfocused goals." ++
+	      (match Proof_global.Bullet.suggest p
+              with None  -> str"" | Some s -> fnl () ++ str s) ++
+              fnl ()
+            in
+	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
 	  end
   | _ -> pr_subgoals None sigma seeds shelf stack goals
   end
diff --git a/printing/printer.mli b/printing/printer.mli
index 6b9c7081..a469a8db 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -128,7 +128,7 @@ val pr_transparent_state   : transparent_state -> std_ppcmds
 (** Proofs *)
 
 val pr_goal                : goal sigma -> std_ppcmds
-val pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
+val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
 val pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds
 val pr_concl               : int -> evar_map -> goal -> std_ppcmds
 
@@ -137,6 +137,8 @@ val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
+val pr_ne_evar_set         : std_ppcmds -> std_ppcmds -> evar_map ->
+  Evar.Set.t -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
@@ -166,7 +168,7 @@ val pr_assumptionset :
 val pr_goal_by_id : string -> std_ppcmds
 
 type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> string option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
+ pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds;
  pr_subgoal             : int -> evar_map -> goal list -> std_ppcmds;
  pr_goal                : goal sigma -> std_ppcmds;
 };;
diff --git a/printing/richprinter.ml b/printing/richprinter.ml
index d71dc82d..d95e1907 100644
--- a/printing/richprinter.ml
+++ b/printing/richprinter.ml
@@ -5,21 +5,20 @@ module RichppVernac = Ppvernac.Richpp
 module RichppTactic = Pptactic.Richpp
 
 type rich_pp =
-    string
-    * Ppannotation.t Richpp.located Xml_datatype.gxml
+    Ppannotation.t Richpp.located Xml_datatype.gxml
     * Xml_datatype.xml
 
 let get_annotations obj = Pp.Tag.prj obj Ppannotation.tag
 
 let make_richpp pr ast =
-  let raw_pp, rich_pp =
+  let rich_pp =
     rich_pp get_annotations (pr ast)
   in
   let xml = Ppannotation.(
     xml_of_rich_pp tag_of_annotation attributes_of_annotation rich_pp
   )
   in
-  (raw_pp, rich_pp, xml)
+  (rich_pp, xml)
 
 let richpp_vernac = make_richpp RichppVernac.pr_vernac
 let richpp_constr = make_richpp RichppConstr.pr_constr_expr
diff --git a/printing/richprinter.mli b/printing/richprinter.mli
index c67d52c0..41c31351 100644
--- a/printing/richprinter.mli
+++ b/printing/richprinter.mli
@@ -20,12 +20,10 @@
 
 (** A rich pretty-print is composed of: *)
 type rich_pp =
-    (** - a raw pretty-print ; *)
-    string
 
     (** - a generalized semi-structured document whose attributes are
         annotations ; *)
-    * Ppannotation.t Richpp.located Xml_datatype.gxml
+    Ppannotation.t Richpp.located Xml_datatype.gxml
 
     (** - an XML document, representing annotations as usual textual
         XML attributes. *)