1 files changed, 73 insertions, 61 deletions

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f22cdbcc..e753e972 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -23,8 +23,9 @@ open Names
 (* Type of proof modes :
     - A function [set] to set it *from standard mode*
     - A function [reset] to reset the *standard mode* from it *)
+type proof_mode_name = string
 type proof_mode = {
-  name : string ;
+  name : proof_mode_name ;
   set : unit -> unit ;
   reset : unit -> unit
 }
@@ -33,10 +34,10 @@ let proof_modes = Hashtbl.create 6
 let find_proof_mode n =
   try Hashtbl.find proof_modes n
   with Not_found ->
-    Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
+    CErrors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (Ephemeron.create m)
+  Hashtbl.add proof_modes n (CEphemeron.create m)
 
 (* initial mode: standard mode *)
 let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
@@ -45,6 +46,9 @@ let _ = register_proof_mode standard
 (* Default proof mode, to be set at the beginning of proofs. *)
 let default_proof_mode = ref (find_proof_mode "No")
 
+let get_default_proof_mode_name () =
+  (CEphemeron.default !default_proof_mode standard).name
+
 let _ =
   Goptions.declare_string_option {Goptions.
     optsync = true ;
@@ -52,7 +56,7 @@ let _ =
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
     optread = begin fun () ->
-      (Ephemeron.default !default_proof_mode standard).name
+      (CEphemeron.default !default_proof_mode standard).name
     end;
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
@@ -83,15 +87,18 @@ type closed_proof = proof_object * proof_terminator
 
 type pstate = {
   pid : Id.t;
-  terminator : proof_terminator Ephemeron.key;
+  terminator : proof_terminator CEphemeron.key;
   endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
-  mode : proof_mode Ephemeron.key;
+  mode : proof_mode CEphemeron.key;
   universe_binders: universe_binders option;
 }
 
+let make_terminator f = f
+let apply_terminator f = f
+
 (* The head of [!pstates] is the actual current proof, the other ones are
    to be resumed when the current proof is closed or aborted. *)
 let pstates = ref ([] : pstate list)
@@ -103,11 +110,11 @@ let current_proof_mode = ref !default_proof_mode
 let update_proof_mode () =
   match !pstates with
   | { mode = m } :: _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := m;
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ())
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
   | _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := find_proof_mode "No"
 
 (* combinators for the current_proof lists *)
@@ -115,15 +122,15 @@ let push a l = l := a::!l;
   update_proof_mode ()
 
 exception NoSuchProof
-let _ = Errors.register_handler begin function
-  | NoSuchProof -> Errors.error "No such proof."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoSuchProof -> CErrors.error "No such proof."
+  | _ -> raise CErrors.Unhandled
 end
 
 exception NoCurrentProof
-let _ = Errors.register_handler begin function
-  | NoCurrentProof -> Errors.error "No focused proof (No proof-editing in progress)."
-  | _ -> raise Errors.Unhandled
+let _ = CErrors.register_handler begin function
+  | NoCurrentProof -> CErrors.error "No focused proof (No proof-editing in progress)."
+  | _ -> raise CErrors.Unhandled
 end
 
 (*** Proof Global manipulation ***)
@@ -183,7 +190,7 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    Errors.error (Pp.string_of_ppcmds
+    CErrors.error (Pp.string_of_ppcmds
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
        str"Use \"Abort All\" first or complete proof(s)."))
   end
@@ -195,7 +202,7 @@ let discard (loc,id) =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
-    Errors.user_err_loc
+    CErrors.user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs ())
 
 let discard_current () =
@@ -215,9 +222,9 @@ let set_proof_mode mn =
   set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
 
 let activate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
-let disactivate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
+let disactivate_current_proof_mode () =
+  CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
 (** [start_proof sigma id str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -230,7 +237,7 @@ let disactivate_proof_mode mode =
 let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.start sigma goals;
     endline_tactic = None;
     section_vars = None;
@@ -242,7 +249,7 @@ let start_proof sigma id ?pl str goals terminator =
 let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start goals;
     endline_tactic = None;
     section_vars = None;
@@ -264,18 +271,19 @@ let _ = Goptions.declare_bool_option
       Goptions.optwrite = (fun b -> proof_using_auto_clear := b) }
 
 let set_used_variables l =
+  let open Context.Named.Declaration in
   let env = Global.env () in
   let ids = List.fold_right Id.Set.add l Id.Set.empty in
   let ctx = Environ.keep_hyps env ids in
   let ctx_set =
-    List.fold_right Id.Set.add (List.map pi1 ctx) Id.Set.empty in
+    List.fold_right Id.Set.add (List.map get_id ctx) Id.Set.empty in
   let vars_of = Environ.global_vars_set in
   let aux env entry (ctx, all_safe, to_clear as orig) =
     match entry with
-    | (x,None,_) ->
+    | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
        else (ctx, all_safe, (Loc.ghost,x)::to_clear) 
-    | (x,Some bo, ty) as decl ->
+    | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
@@ -288,7 +296,7 @@ let set_used_variables l =
   | [] -> raise NoCurrentProof
   | p :: rest ->
       if not (Option.is_empty p.section_vars) then
-        Errors.error "Used section variables can be declared only once";
+        CErrors.error "Used section variables can be declared only once";
       pstates := { p with section_vars = Some ctx} :: rest;
       ctx, to_clear
 
@@ -299,6 +307,11 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
+let constrain_variables init uctx =
+  let levels = Univ.Instance.levels (Univ.UContext.instance init) in
+  let cstrs = UState.constrain_variables levels uctx in
+  Univ.ContextSet.add_constraints cstrs (UState.context_set uctx)
+
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
@@ -329,7 +342,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
           let initunivs = Evd.evar_context_universe_context initial_euctx in
-          let ctx = Evd.evar_universe_context_set initunivs universes in
+          let ctx = constrain_variables initunivs universes in
           (* For vi2vo compilation proofs are computed now but we need to
            * complement the univ constraints of the typ with the ones of
            * the body.  So we keep the two sets distinct. *)
@@ -338,7 +351,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
           (initunivs, typ), ((body, ctx_body), eff)
         else
           let initunivs = Univ.UContext.empty in
-          let ctx = Evd.evar_universe_context_set initunivs universes in
+          let ctx = constrain_variables initunivs universes in
           (* Since the proof is computed now, we can simply have 1 set of
            * constraints in which we merge the ones for the body and the ones
            * for the typ *)
@@ -353,7 +366,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
         let initunivs = Evd.evar_context_universe_context initial_euctx in
         Future.from_val (initunivs, nf t),
         Future.chain ~pure:true p (fun (pt,eff) ->
-          (pt,Evd.evar_universe_context_set initunivs (Future.force univs)),eff)
+          (pt,constrain_variables initunivs (Future.force univs)),eff)
   in
   let entries =
     Future.map2 (fun p (_, t) ->
@@ -375,7 +388,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
-  fun pr_ending -> Ephemeron.get terminator pr_ending
+  fun pr_ending -> CEphemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
@@ -395,7 +408,7 @@ let return_proof ?(allow_partial=false) () =
   let evd =
     let error s =
       let prf = str " (in proof " ++ Id.print pid ++ str ")" in
-      raise (Errors.UserError("last tactic before Qed",s ++ prf))
+      raise (CErrors.UserError("last tactic before Qed",s ++ prf))
     in
     try Proof.return proof with
     | Proof.UnfinishedProof ->
@@ -423,11 +436,11 @@ let close_proof ~keep_body_ucst_separate fix_exn =
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator
+let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator
 let set_terminator hook =
   match !pstates with
   | [] -> raise NoCurrentProof
-  | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
+  | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
 
 
@@ -458,7 +471,7 @@ module Bullet = struct
   type behavior = {
     name : string;
     put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> string option
+    suggest: Proof.proof -> std_ppcmds
   }
 
   let behaviors = Hashtbl.create 4
@@ -468,7 +481,7 @@ module Bullet = struct
   let none = {
     name = "None";
     put = (fun x _ -> x);
-    suggest = (fun _ -> None)
+    suggest = (fun _ -> mt ())
   }
   let _ = register_behavior none
 
@@ -484,36 +497,30 @@ module Bullet = struct
     (* give a message only if more informative than the standard coq message *)
     let suggest_on_solved_goal sugg =
       match sugg with
-      | NeedClosingBrace -> Some "Try unfocusing with \"}\"."
-      | NoBulletInUse -> None
-      | ProofFinished -> None
-      | Suggest b -> Some ("Focus next goal with bullet "
-			   ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			   ^".")
-      | Unfinished b -> Some ("The current bullet "
-			      ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			      ^ " is unfinished.")
+      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
+      | NoBulletInUse -> mt ()
+      | ProofFinished -> mt ()
+      | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
+      | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
 
     (* give always a message. *)
     let suggest_on_error sugg =
       match sugg with
-      | NeedClosingBrace -> "Try unfocusing with \"}\"."
+      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
       | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> "No more subgoals."
-      | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-		      ^ " is mandatory here.")
-      | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b))
-			 ^ " is not finished.")
+      | ProofFinished -> str"No more subgoals."
+      | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+      | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
 
     exception FailedBullet of t * suggestion
 
     let _ =
-      Errors.register_handler
+      CErrors.register_handler
 	(function
 	| FailedBullet (b,sugg) ->
-	  let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (Pp.(pr_bullet b)) ^ " : " in
-	  Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg))
-	| _ -> raise Errors.Unhandled)
+	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+	  CErrors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
+	| _ -> raise CErrors.Unhandled)
 
 
     (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
@@ -610,7 +617,7 @@ module Bullet = struct
     let _ = register_behavior strict
   end
 
-  (* Current bullet behavior, controled by the option *)
+  (* Current bullet behavior, controlled by the option *)
   let current_behavior = ref Strict.strict
 
   let _ =
@@ -626,7 +633,7 @@ module Bullet = struct
 	current_behavior :=
           try Hashtbl.find behaviors n
           with Not_found ->
-            Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
+            CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
     }
 
@@ -657,21 +664,26 @@ let _ =
 let default_goal_selector = ref (Vernacexpr.SelectNth 1)
 let get_default_goal_selector () = !default_goal_selector
 
+let print_range_selector (i, j) =
+  if i = j then string_of_int i
+  else string_of_int i ^ "-" ^ string_of_int j
+
 let print_goal_selector = function
   | Vernacexpr.SelectAll -> "all"
   | Vernacexpr.SelectNth i -> string_of_int i
+  | Vernacexpr.SelectList l -> "[" ^
+      String.concat ", " (List.map print_range_selector l) ^ "]"
   | Vernacexpr.SelectId id -> Id.to_string id
-  | Vernacexpr.SelectAllParallel -> "par"
 
 let parse_goal_selector = function
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "A selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\" or a natural number." in
       begin try
               let i = int_of_string i in
-              if i < 0 then Errors.error err_msg;
+              if i < 0 then CErrors.error err_msg;
               Vernacexpr.SelectNth i
-        with Failure _ -> Errors.error err_msg
+        with Failure _ -> CErrors.error err_msg
       end
 
 let _ =
@@ -700,7 +712,7 @@ type state = pstate list
 let freeze ~marshallable =
   match marshallable with
   | `Yes ->
-      Errors.anomaly (Pp.str"full marshalling of proof state not supported")
+      CErrors.anomaly (Pp.str"full marshalling of proof state not supported")
   | `Shallow -> !pstates
   | `No -> !pstates
 let unfreeze s = pstates := s; update_proof_mode ()