Proofview: split [V82] module into [Unsafe] and [V82].

The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.

3 files changed, 179 insertions, 163 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 76fc37d37..7d25bb665 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -123,7 +123,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
     let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
-	Proofview.V82.tclEVARSADVANCE evd'
+	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when Errors.noncritical e ->
       (** This is Tacticals.tclFAIL *)
       Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a3f58396f..4a83ed6d2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -864,57 +864,7 @@ let in_proofview p k =
 let reset_future_goals p =
   { p with solution = Evd.reset_future_goals p.solution }
 
-
-module Notations = struct
-  let (>>=) = tclBIND
-  let (<*>) = tclTHEN
-  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-end
-
-open Notations
-
-module Monad =
-  Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end)
-
-
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 = struct
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-
-  let tactic tac =
-    (* spiwack: we ignore the dependencies between goals here,
-       expectingly preserving the semantics of <= 8.2 tactics *)
-    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-    let (>>=) = Proof.bind in
-    Pv.get >>= fun ps ->
-    try
-      let tac gl evd = 
-        let glsigma  =
-          tac { Evd.it = gl ; sigma = evd; }  in
-        let sigma = glsigma.Evd.sigma in
-        let g = glsigma.Evd.it in
-        ( g, sigma )
-      in
-        (* Old style tactics expect the goals normalized with respect to evars. *)
-      let (initgoals,initevd) =
-        Evd.Monad.List.map (fun g s -> Goal.V82.nf_evar s g) ps.comb ps.solution
-      in
-      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
-      let sgs = List.flatten goalss in
-      Pv.set { solution = evd; comb = sgs; }
-    with e when catchable_exception e ->
-      let e = Errors.push e in
-      tclZERO e
-
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  let nf_evar_goals =
-    Pv.modify begin fun ps ->
-    let map g s = Goal.V82.nf_evar s g in
-    let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
-    { solution = evd; comb = goals; }
-    end
+module Unsafe = struct
 
   (* A [Proofview.tactic] version of [Refiner.tclEVARS] *)
   let tclEVARS evd =
@@ -925,66 +875,22 @@ module V82 = struct
 
   let tclEVARUNIVCONTEXT ctx = 
     Pv.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx })
-      
-  let has_unresolved_evar pv =
-    Evd.has_undefined pv.solution
-
-  (* Main function in the implementation of Grab Existential Variables.*)
-  let grab pv =
-    let undef = Evd.undefined_map pv.solution in
-    let goals = List.rev_map fst (Evar.Map.bindings undef) in
-    { pv with comb = goals }
-      
-    
 
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
-  let goals { comb = comb ; solution = solution; } =
-   { Evd.it = comb ; sigma = solution }
-
-  let top_goals initial { solution=solution; } =
-    let goals = List.map (fun (t,_) -> fst (Term.destEvar t)) initial in
-    { Evd.it = goals ; sigma=solution; }
-
-  let top_evars initial =
-    let evars_of_initial (c,_) =
-      Evar.Set.elements (Evd.evars_of_term c)
-    in
-    List.flatten (List.map evars_of_initial initial)
-
-  let instantiate_evar n com pv =
-    let (evk,_) =
-      let evl = Evarutil.non_instantiated pv.solution in
-      let evl = Evar.Map.bindings evl in
-      if (n <= 0) then
-	Errors.error "incorrect existential variable index"
-      else if List.length evl < n then
-	  Errors.error "not so many uninstantiated existential variables"
-      else
-	List.nth evl (n-1) 
-    in
-    { pv with
-	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
-
-  let of_tactic t gls =
-    try
-      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
-      let (_,final,_) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
-      { Evd.sigma = final.solution ; it = final.comb }
-    with Proofview_monad.TacticFailure e as src ->
-      let src = Errors.push src in
-      let e = Backtrace.app_backtrace ~src ~dst:e in
-      raise e
+end
 
-  let put_status = Status.put
+module Notations = struct
+  let (>>=) = tclBIND
+  let (<*>) = tclTHEN
+  let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
+end
 
-  let catchable_exception = catchable_exception
+open Notations
 
-  let wrap_exceptions f =
-    try f ()
-    with e when catchable_exception e -> let e = Errors.push e in tclZERO e
+module Monad =
+  Monad.Make(struct type +'a t = 'a tactic let return=tclUNIT let (>>=)=(>>=) end)
 
-end
+(* To avoid shadowing by the local [Goal] module *)
+module GoalV82 = Goal.V82
 
 module Goal = struct
 
@@ -1022,7 +928,7 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try
         let (gl, sigma) = nf_gmake env sigma goal in
-        tclTHEN (V82.tclEVARS sigma) (f gl)
+        tclTHEN (Unsafe.tclEVARS sigma) (f gl)
       with e when catchable_exception e ->
         let e = Errors.push e in
         tclZERO e
@@ -1032,7 +938,7 @@ module Goal = struct
     Env.get >>= fun env ->
     tclEVARMAP >>= fun sigma ->
     let (gl,sigma) = nf_gmake env sigma self in
-    tclTHEN (V82.tclEVARS sigma) (tclUNIT gl)
+    tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl)
 
   let gmake env sigma goal =
     let info = Evd.find sigma goal in
@@ -1148,3 +1054,106 @@ let tclLIFT = Proof.lift
 
 let tclCHECKINTERRUPT =
    tclLIFT (NonLogical.make Control.check_for_interrupt)
+
+
+
+
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 = struct
+  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
+
+  let tactic tac =
+    (* spiwack: we ignore the dependencies between goals here,
+       expectingly preserving the semantics of <= 8.2 tactics *)
+    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+    let (>>=) = Proof.bind in
+    Pv.get >>= fun ps ->
+    try
+      let tac gl evd = 
+        let glsigma  =
+          tac { Evd.it = gl ; sigma = evd; }  in
+        let sigma = glsigma.Evd.sigma in
+        let g = glsigma.Evd.it in
+        ( g, sigma )
+      in
+        (* Old style tactics expect the goals normalized with respect to evars. *)
+      let (initgoals,initevd) =
+        Evd.Monad.List.map (fun g s -> GoalV82.nf_evar s g) ps.comb ps.solution
+      in
+      let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
+      let sgs = List.flatten goalss in
+      Pv.set { solution = evd; comb = sgs; }
+    with e when catchable_exception e ->
+      let e = Errors.push e in
+      tclZERO e
+
+
+  (* normalises the evars in the goals, and stores the result in
+     solution. *)
+  let nf_evar_goals =
+    Pv.modify begin fun ps ->
+    let map g s = GoalV82.nf_evar s g in
+    let (goals,evd) = Evd.Monad.List.map map ps.comb ps.solution in
+    { solution = evd; comb = goals; }
+    end
+      
+  let has_unresolved_evar pv =
+    Evd.has_undefined pv.solution
+
+  (* Main function in the implementation of Grab Existential Variables.*)
+  let grab pv =
+    let undef = Evd.undefined_map pv.solution in
+    let goals = List.rev_map fst (Evar.Map.bindings undef) in
+    { pv with comb = goals }
+      
+    
+
+  (* Returns the open goals of the proofview together with the evar_map to 
+     interprete them. *)
+  let goals { comb = comb ; solution = solution; } =
+   { Evd.it = comb ; sigma = solution }
+
+  let top_goals initial { solution=solution; } =
+    let goals = List.map (fun (t,_) -> fst (Term.destEvar t)) initial in
+    { Evd.it = goals ; sigma=solution; }
+
+  let top_evars initial =
+    let evars_of_initial (c,_) =
+      Evar.Set.elements (Evd.evars_of_term c)
+    in
+    List.flatten (List.map evars_of_initial initial)
+
+  let instantiate_evar n com pv =
+    let (evk,_) =
+      let evl = Evarutil.non_instantiated pv.solution in
+      let evl = Evar.Map.bindings evl in
+      if (n <= 0) then
+	Errors.error "incorrect existential variable index"
+      else if List.length evl < n then
+	  Errors.error "not so many uninstantiated existential variables"
+      else
+	List.nth evl (n-1) 
+    in
+    { pv with
+	solution = Evar_refiner.instantiate_pf_com evk com pv.solution }
+
+  let of_tactic t gls =
+    try
+      let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] } in
+      let (_,final,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
+      { Evd.sigma = final.solution ; it = final.comb }
+    with Proofview_monad.TacticFailure e as src ->
+      let src = Errors.push src in
+      let e = Backtrace.app_backtrace ~src ~dst:e in
+      raise e
+
+  let put_status = Status.put
+
+  let catchable_exception = catchable_exception
+
+  let wrap_exceptions f =
+    try f ()
+    with e when catchable_exception e -> let e = Errors.push e in tclZERO e
+
+end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 7f070d006..cb0df1853 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -307,6 +307,19 @@ val tclTIME : string option -> 'a tactic -> 'a tactic
 (** [mark_as_unsafe] signals that the current tactic is unsafe. *)
 val mark_as_unsafe : unit tactic
 
+module Unsafe : sig
+
+  (* Assumes the new evar_map does not change existing goals *)
+  val tclEVARS : Evd.evar_map -> unit tactic
+    
+  (* Assumes the new evar_map might be solving some existing goals *)
+  val tclEVARSADVANCE : Evd.evar_map -> unit tactic
+
+  (* Set the evar universe context *)
+  val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
+
+end
+
 module Monad : Monad.S with type +'a t = 'a tactic
 
 (*** Commands ***)
@@ -326,60 +339,6 @@ module Notations : sig
 end
 
 
-(*** Compatibility layer with <= 8.2 tactics ***)
-module V82 : sig
-  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
-  val tactic : tac -> unit tactic
-
-  (* normalises the evars in the goals, and stores the result in
-     solution. *)
-  val nf_evar_goals : unit tactic
-    
-  (* Assumes the new evar_map does not change existing goals *)
-  val tclEVARS : Evd.evar_map -> unit tactic
-    
-  (* Assumes the new evar_map might be solving some existing goals *)
-  val tclEVARSADVANCE : Evd.evar_map -> unit tactic
-
-  (* Set the evar universe context *)
-  val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic
-
-  val has_unresolved_evar : proofview -> bool
-
-  (* Main function in the implementation of Grab Existential Variables.
-     Resets the proofview's goals so that it contains all unresolved evars
-     (in chronological order of insertion). *)
-  val grab : proofview -> proofview
-
-  (* Returns the open goals of the proofview together with the evar_map to 
-     interprete them. *)
-  val goals : proofview -> Evar.t list Evd.sigma
-
-  val top_goals : entry -> proofview -> Evar.t list Evd.sigma
-  
-  (* returns the existential variable used to start the proof *)
-  val top_evars : entry -> Evd.evar list
-    
-  (* Implements the Existential command *)
-  val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
-
-  (* Caution: this function loses quite a bit of information. It
-     should be avoided as much as possible.  It should work as
-     expected for a tactic obtained from {!V82.tactic} though. *)
-  val of_tactic : 'a tactic -> tac
-
-  (* marks as unsafe if the argument is [false] *)
-  val put_status : bool -> unit tactic
-
-  (* exception for which it is deemed to be safe to transmute into
-     tactic failure. *)
-  val catchable_exception : exn -> bool
-
-  (* transforms every Ocaml (catchable) exception into a failure in
-     the monad. *)
-  val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
-end
-
 (* The module goal provides an interface for goal-dependent tactics. *)
 (* spiwack: there are still parts of the code which depend on proofs/goal.ml.
    Eventually I'll try to remove it in favour of [Proofview.Goal] *)
@@ -506,3 +465,51 @@ end
 
 (* [tclLIFT c] includes the non-logical command [c] in a tactic. *)
 val tclLIFT : 'a NonLogical.t -> 'a tactic
+
+
+
+
+(*** Compatibility layer with <= 8.2 tactics ***)
+module V82 : sig
+  type tac = Evar.t Evd.sigma -> Evar.t list Evd.sigma
+  val tactic : tac -> unit tactic
+
+  (* normalises the evars in the goals, and stores the result in
+     solution. *)
+  val nf_evar_goals : unit tactic
+
+  val has_unresolved_evar : proofview -> bool
+
+  (* Main function in the implementation of Grab Existential Variables.
+     Resets the proofview's goals so that it contains all unresolved evars
+     (in chronological order of insertion). *)
+  val grab : proofview -> proofview
+
+  (* Returns the open goals of the proofview together with the evar_map to 
+     interprete them. *)
+  val goals : proofview -> Evar.t list Evd.sigma
+
+  val top_goals : entry -> proofview -> Evar.t list Evd.sigma
+  
+  (* returns the existential variable used to start the proof *)
+  val top_evars : entry -> Evd.evar list
+    
+  (* Implements the Existential command *)
+  val instantiate_evar : int -> Constrexpr.constr_expr -> proofview -> proofview
+
+  (* Caution: this function loses quite a bit of information. It
+     should be avoided as much as possible.  It should work as
+     expected for a tactic obtained from {!V82.tactic} though. *)
+  val of_tactic : 'a tactic -> tac
+
+  (* marks as unsafe if the argument is [false] *)
+  val put_status : bool -> unit tactic
+
+  (* exception for which it is deemed to be safe to transmute into
+     tactic failure. *)
+  val catchable_exception : exn -> bool
+
+  (* transforms every Ocaml (catchable) exception into a failure in
+     the monad. *)
+  val wrap_exceptions : (unit -> 'a tactic) -> 'a tactic
+end