1 files changed, 54 insertions, 64 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5bcb3b1e1..10c139e5a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -56,20 +56,19 @@ let scope_class_of_qualid qid =
 let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
+  let sigma, env = Pfedit.get_current_context () in
   let pprf = Proof.partial_proof p in
-  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl Printer.pr_econstr pprf)
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
 
 let show_top_evars () =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
   let pfts = Proof_global.give_me_the_proof () in
-  let gls = Proof.V82.subgoals pfts in
-  let sigma = gls.Evd.sigma in
+  let gls,_,_,_,sigma = Proof.proof pfts in
   Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma))
 
 let show_universes () =
   let pfts = Proof_global.give_me_the_proof () in
-  let gls = Proof.V82.subgoals pfts in
-  let sigma = gls.Evd.sigma in
+  let gls,_,_,_,sigma = Proof.proof pfts in
   let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in
     Feedback.msg_notice (Termops.pr_evar_universe_context (Evd.evar_universe_context sigma));
     Feedback.msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Termops.pr_evd_level sigma) ctx)
@@ -78,7 +77,7 @@ let show_universes () =
 let show_intro all =
   let open EConstr in
   let pf = Proof_global.give_me_the_proof() in
-  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gls,_,_,_,sigma = Proof.proof pf in
   if not (List.is_empty gls) then begin
     let gl = {Evd.it=List.hd gls ; sigma = sigma; } in
     let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in
@@ -257,7 +256,8 @@ let print_namespace ns =
   let print_constant k body =
     (* FIXME: universes *)
     let t = body.Declarations.const_type in
-    print_kn k ++ str":" ++ spc() ++ Printer.pr_type t
+    let sigma, env = Pfedit.get_current_context () in
+    print_kn k ++ str":" ++ spc() ++ Printer.pr_type_env env sigma t
   in
   let matches mp = match match_modulepath ns mp with
   | Some [] -> true
@@ -486,8 +486,8 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
  	let red_option = match red_option with
           | None -> None
           | Some r ->
-	      let (evc,env)= get_current_context () in
- 		Some (snd (Hook.get f_interp_redexp env evc r)) in
+            let sigma, env= Pfedit.get_current_context () in
+            Some (snd (Hook.get f_interp_redexp env sigma r)) in
 	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l =
@@ -1539,7 +1539,7 @@ let vernac_print_option key =
 
 let get_current_context_of_args = function
   | Some n -> Pfedit.get_goal_context n
-  | None -> get_current_context ()
+  | None -> Pfedit.get_current_context ()
 
 let query_command_selector ?loc = function
   | None -> None
@@ -1601,7 +1601,7 @@ let vernac_global_check c =
 
 let get_nth_goal n =
   let pf = Proof_global.give_me_the_proof() in
-  let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in
+  let gls,_,_,_,sigma = Proof.proof pf in
   let gl = {Evd.it=List.nth gls (n-1) ; sigma = sigma; } in
   gl
   
@@ -1628,17 +1628,20 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt =
     let natureofid = match decl with
                      | LocalAssum _ -> "Hypothesis"
                      | LocalDef (_,bdy,_) ->"Constant (let in)" in
-    v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl()
+    let sigma, env = Pfedit.get_current_context () in
+    v 0 (Id.print id ++ str":" ++ pr_econstr_env env sigma (NamedDecl.get_type decl) ++ fnl() ++ fnl()
 	 ++ str natureofid ++ str " of the goal context.")
   with (* fallback to globals *)
-    | NoHyp | Not_found -> print_about ref_or_by_not
+    | NoHyp | Not_found ->
+    let sigma, env = Pfedit.get_current_context () in
+    print_about env sigma ref_or_by_not
 
-	       
-let vernac_print ?loc = let open Feedback in function
+
+let vernac_print ?loc env sigma = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
-  | PrintFullContext-> msg_notice (print_full_context_typ ())
-  | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
-  | PrintInspect n -> msg_notice (inspect n)
+  | PrintFullContext-> msg_notice (print_full_context_typ env sigma)
+  | PrintSectionContext qid -> msg_notice (print_sec_context_typ env sigma qid)
+  | PrintInspect n -> msg_notice (inspect env sigma n)
   | PrintGrammar ent -> msg_notice (Metasyntax.pr_grammar ent)
   | PrintLoadPath dir -> (* For compatibility ? *) msg_notice (print_loadpath dir)
   | PrintModules -> msg_notice (print_modules ())
@@ -1648,15 +1651,15 @@ let vernac_print ?loc = let open Feedback in function
   | PrintMLLoadPath -> msg_notice (Mltop.print_ml_path ())
   | PrintMLModules -> msg_notice (Mltop.print_ml_modules ())
   | PrintDebugGC -> msg_notice (Mltop.print_gc ())
-  | PrintName qid -> dump_global qid; msg_notice (print_name qid)
+  | PrintName qid -> dump_global qid; msg_notice (print_name env sigma qid)
   | PrintGraph -> msg_notice (Prettyp.print_graph())
   | PrintClasses -> msg_notice (Prettyp.print_classes())
   | PrintTypeClasses -> msg_notice (Prettyp.print_typeclasses())
   | PrintInstances c -> msg_notice (Prettyp.print_instances (smart_global c))
-  | PrintCoercions -> msg_notice (Prettyp.print_coercions())
+  | PrintCoercions -> msg_notice (Prettyp.print_coercions env sigma)
   | PrintCoercionPaths (cls,clt) ->
       msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
-  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ())
+  | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections env sigma)
   | PrintUniverses (b, dst) ->
      let univ = Global.universes () in
      let univ = if b then UGraph.sort_universes univ else univ in
@@ -1668,16 +1671,16 @@ let vernac_print ?loc = let open Feedback in function
      | None -> msg_notice (UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining)
      | Some s -> dump_universes_gen univ s
      end
-  | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r))
+  | PrintHint r -> msg_notice (Hints.pr_hint_ref env sigma (smart_global r))
   | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ())
-  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name s)
-  | PrintHintDb -> msg_notice (Hints.pr_searchtable ())
+  | PrintHintDbName s -> msg_notice (Hints.pr_hint_db_by_name env sigma s)
+  | PrintHintDb -> msg_notice (Hints.pr_searchtable env sigma)
   | PrintScopes ->
-      msg_notice (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
+      msg_notice (Notation.pr_scopes (Constrextern.without_symbols (pr_lglob_constr_env env)))
   | PrintScope s ->
-      msg_notice (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_scope (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintVisibility s ->
-      msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_notice (Notation.pr_visibility (Constrextern.without_symbols (pr_lglob_constr_env env)) s)
   | PrintAbout (ref_or_by_not,glnumopt) ->
      msg_notice (print_about_hyp_globs ?loc ref_or_by_not glnumopt)
   | PrintImplicit qid ->
@@ -1780,9 +1783,10 @@ let vernac_locate = let open Feedback in function
   | LocateTerm (AN qid) -> msg_notice (print_located_term qid)
   | LocateAny (ByNotation (_, (ntn, sc))) (** TODO : handle Ltac notations *)
   | LocateTerm (ByNotation (_, (ntn, sc))) ->
-      msg_notice
-        (Notation.locate_notation
-          (Constrextern.without_symbols pr_lglob_constr) ntn sc)
+    let _, env = Pfedit.get_current_context () in
+    msg_notice
+      (Notation.locate_notation
+         (Constrextern.without_symbols (pr_lglob_constr_env env)) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> msg_notice (print_located_module qid)
   | LocateOther (s, qid) -> msg_notice (print_located_other s qid)
@@ -1849,10 +1853,11 @@ let vernac_bullet (bullet : Proof_bullet.t) =
 let vernac_show = let open Feedback in function
   | ShowScript -> assert false  (* Only the stm knows the script *)
   | ShowGoal goalref ->
+    let proof = Proof_global.give_me_the_proof () in
     let info = match goalref with
-      | OpenSubgoals -> pr_open_subgoals ()
-      | NthGoal n -> pr_nth_open_subgoal n
-      | GoalId id -> pr_goal_by_id id
+      | OpenSubgoals -> pr_open_subgoals ~proof
+      | NthGoal n -> pr_nth_open_subgoal ~proof n
+      | GoalId id -> pr_goal_by_id ~proof id
     in
     msg_notice info
   | ShowProof -> show_proof ()
@@ -1909,7 +1914,7 @@ let vernac_load interp fname =
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-let interp ?proof ?loc locality poly c =
+let interp ?proof ?loc locality poly st c =
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
   match c with
   (* The below vernac are candidates for removal from the main type
@@ -2043,7 +2048,9 @@ let interp ?proof ?loc locality poly c =
   | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ?loc r g c
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
-  | VernacPrint p -> vernac_print ?loc p
+  | VernacPrint p ->
+    let sigma, env = Pfedit.get_current_context () in
+    vernac_print ?loc env sigma p
   | VernacSearch (s,g,r) -> vernac_search ?loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
@@ -2069,7 +2076,10 @@ let interp ?proof ?loc locality poly c =
   | VernacProofMode mn -> Proof_global.set_proof_mode mn [@ocaml.warning "-3"]
 
   (* Extensions *)
-  | VernacExtend (opn,args) -> Vernacinterp.call ?locality ?loc (opn,args)
+  | VernacExtend (opn,args) ->
+    (* XXX: Here we are returning the state! :) *)
+    let _st : Vernacstate.t = Vernacinterp.call ?locality ?loc (opn,args) st in
+    ()
 
 (* Vernaculars that take a locality flag *)
 let check_vernac_supports_locality c l =
@@ -2147,28 +2157,6 @@ let locate_if_not_already ?loc (e, info) =
 exception HasNotFailed
 exception HasFailed of Pp.t
 
-type interp_state = { (* TODO: inline records in OCaml 4.03 *)
-  system  : States.state;        (* summary + libstack *)
-  proof   : Proof_global.state;  (* proof state *)
-  shallow : bool                 (* is the state trimmed down (libstack) *)
-}
-
-let s_cache = ref (States.freeze ~marshallable:`No)
-let s_proof = ref (Proof_global.freeze ~marshallable:`No)
-
-let invalidate_cache () =
-  s_cache := Obj.magic 0;
-  s_proof := Obj.magic 0
-
-let freeze_interp_state marshallable =
-  { system = (s_cache := States.freeze ~marshallable; !s_cache);
-    proof  = (s_proof := Proof_global.freeze ~marshallable; !s_proof);
-    shallow = marshallable = `Shallow }
-
-let unfreeze_interp_state { system; proof } =
-  if (!s_cache != system) then (s_cache := system; States.unfreeze system);
-  if (!s_proof != proof)  then (s_proof := proof;  Proof_global.unfreeze proof)
-
 (* XXX STATE: this type hints that restoring the state should be the
    caller's responsibility *)
 let with_fail st b f =
@@ -2187,8 +2175,8 @@ let with_fail st b f =
                             (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e)))
     with e when CErrors.noncritical e ->
       (* Restore the previous state XXX Careful here with the cache! *)
-      invalidate_cache ();
-      unfreeze_interp_state st;
+      Vernacstate.invalidate_cache ();
+      Vernacstate.unfreeze_interp_state st;
       let (e, _) = CErrors.push e in
       match e with
       | HasNotFailed ->
@@ -2230,8 +2218,8 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
         try
           vernac_timeout begin fun () ->
           if verbosely
-            then Flags.verbosely (interp ?proof ?loc locality poly) c
-            else Flags.silently  (interp ?proof ?loc locality poly) c;
+            then Flags.verbosely (interp ?proof ?loc locality poly st) c
+            else Flags.silently  (interp ?proof ?loc locality poly st) c;
           if orig_program_mode || not !Flags.program_mode || isprogcmd then
             Flags.program_mode := orig_program_mode;
 	  ignore (Flags.use_polymorphic_flag ())
@@ -2252,7 +2240,9 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
     if verbosely then Flags.verbosely (aux false) c
     else aux false c
 
+(* XXX: There is a bug here in case of an exception, see @gares
+   comments on the PR *)
 let interp ?verbosely ?proof st cmd =
-  unfreeze_interp_state st;
+  Vernacstate.unfreeze_interp_state st;
   interp ?verbosely ?proof st cmd;
-  freeze_interp_state `No
+  Vernacstate.freeze_interp_state `No