Getting rid of Goal.here, and all the related exceptions and combinators.

It was a bad idea. The new API based on lists seems more sensible.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16969 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 153 insertions, 201 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 988c10d27..da5cb6b19 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -352,39 +352,6 @@ let env env _ _ _ = env
 let defs _ rdefs _ _ =
   !rdefs
 
-(* Cf mli for more detailed comment.
-    [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
-    to communicate whether or not the value is defined in the particular context. *)
-exception UndefinedHere
-(* no handler: this should never be allowed to reach toplevel *)
-let null _ _ _ _ = raise UndefinedHere
-
-let plus s1 s2 env rdefs goal info =
-  try s1 env rdefs goal info
-  with UndefinedHere -> s2 env rdefs goal info
-
-(* Equality of two goals *)
-let equal_pointer { content = e1 } { content = e2 } = Evar.equal e1 e2
-
-let here goal value _ _ goal' _ =
-  if equal_pointer goal goal' then
-    value
-  else
-    raise UndefinedHere
-
-(* arnaud: voir à la passer dans Util ? *)
-let rec list_mem_with eq x = function
-  | y::_ when eq x y -> true
-  | _::l -> list_mem_with eq x l
-  | [] -> false
-
-let here_list goals value _ _ goal' _ =
-  if list_mem_with equal_pointer goal' goals then
-    value
-  else
-    raise UndefinedHere
-
-
 (*** Conversion in goals ***)
 
 let convert_hyp check (id,b,bt as d) env rdefs gl info =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 718d23ccc..216e12f3a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -147,30 +147,6 @@ val env : Environ.env sensitive
 (* [defs] is the [Evd.evar_map] at the current evaluation point *)
 val defs : Evd.evar_map sensitive
 
-(* These four functions serve as foundation for the goal sensitive part
-    of the tactic monad (see Proofview).
-    [here] is a special sort of [return]: [here g a] is the value [a], but
-    does not have any value (it raises an exception) if evaluated in
-    any other goal than [g].
-    [here_list] is the same, except with a list of goals rather than a single one.
-    [plus a b] is the same as [a] if [a] is defined in the current goal, otherwise
-    it is [b]. Effectively it's defined in the goals where [a] and [b] are defined.
-    [null] is defined in no goal. (it is a neutral element for [plus]). *)
-(* spiwack: these primitives are a bit hackish, but I couldn't find another way
-    to pass information between goals, like for an intro tactic which gives to
-    each goal the name of the variable it introduce.
-    In pratice, in my experience, the primitives given in Proofview (in terms of
-    [here] and [plus]) are sufficient to define any tactics, hence these might
-    be another example of communication primitives between Goal and Proofview.
-    Still, I can't see a way to prevent using the Proofview primitive to read
-    a goal sensitive value out of its valid context. *)
-val null : 'a sensitive
-
-val plus : 'a sensitive -> 'a sensitive -> 'a sensitive 
-
-val here : goal -> 'a -> 'a sensitive 
-
-val here_list : goal list -> 'a -> 'a sensitive 
 
 (*** Additional functions ***)
 
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 712845f58..89f3638a1 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -252,7 +252,7 @@ let initial_goals p = Proofview.initial_goals p.proofview
 
 let run_tactic env tac pr =
   let sp = pr.proofview in
-  let tacticced_proofview = Proofview.apply env tac sp in
+  let (_,tacticced_proofview) = Proofview.apply env tac sp in
   { pr with proofview = tacticced_proofview }
 
 let emit_side_effects eff pr =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 388778ff7..1fbce62df 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -201,7 +201,7 @@ type +'a tactic = Environ.env -> 'a Inner.t
 (* Applies a tactic to the current proofview. *)
 let apply env t sp =
   let next = Backtrack.run (Inner.run (t env) sp) in
-  next.Inner.state
+  next.Inner.result , next.Inner.state
 
 (*** tacticals ***)
 
@@ -272,15 +272,10 @@ let tclFOCUS i j t env =
 
 (* arnaud: vérifier les commentaires de dispatch vis-à-vis de l'ordre
    d'évaluation des buts. Ne pas oublier le mli *)
+(* arnaud: commenter [tclDISPATCHL] *)
 (* Dispatch tacticals are used to apply a different tactic to each goal under
    consideration. They come in two flavours:
-   [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic].
-   [tclDISPATCHS] takes a list of ['a sensitive tactic] and returns and returns
-   and ['a sensitive tactic] where the ['a sensitive] interpreted in a goal [g]
-   corresponds to that of the tactic which created [g].
-   It is to be noted that the return value of [tclDISPATCHS ts] makes only
-   sense in the goals immediatly built by it, and would cause an anomaly
-   is used otherwise. *)
+   [tclDISPATCH] takes a list of [unit tactic]-s and build a [unit tactic]. *)
 exception SizeMismatch
 let _ = Errors.register_handler begin function
   | SizeMismatch -> Errors.error "Incorrect number of goals."
@@ -312,31 +307,12 @@ let rec tclDISPATCHGEN null join tacs env =
       tclDISPATCHGEN null join tacs env >>= fun x ->
       Inner.get >>= fun step' ->
       Inner.set {step' with comb=step.comb@step'.comb} >>
-      Inner.return (join x y)
+      Inner.return (join y x)
   | _ , _ -> tclZERO SizeMismatch env
 
 let unitK () () = ()
 let tclDISPATCH = tclDISPATCHGEN () unitK
 
-(* This is a helper function for the dispatching tactics (like [tclGOALBIND] and
-    [tclDISPATCHS]). It takes an ['a sensitive] value, and returns a tactic
-    whose return value is, again, ['a sensitive] but only has value in the
-    (unmodified) goals under focus. *)
-let here_s b env =
-  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  Inner.get >>= fun step ->
-  Inner.return (Goal.bind (Goal.here_list step.comb b) (fun b -> b))
-
-(* see .mli for documentation. *)
-let tclDISPATCHS tacs = 
-  let tacs = 
-    List.map begin fun tac ->
-      tclBIND tac here_s
-    end tacs 
-  in
-  tclDISPATCHGEN Goal.null Goal.plus tacs
-
 let tclDISPATCHL tacs =
   let tacs =
     List.map begin fun tac ->
@@ -363,43 +339,6 @@ let tclEXTEND tacs1 rtac tacs2 env =
   let tacs = extend_to_list tacs1 rtac tacs2 step.comb in
   tclDISPATCH tacs env
 
-(* [tclGOALBIND] and [tclGOALBINDU] are sorts of bind which take a
-    [Goal.sensitive] as a first argument, the tactic then acts on each goal separately.
-    Allows backtracking between goals. *)
-
-(* [list_of_sensitive s k] where [s] is and ['a Goal.sensitive] [k]
-   has type ['a -> 'b] returns the list of ['b] obtained by evualating
-   [s] to each goal successively and applying [k] to each result. *)
-let list_of_sensitive s k env step =
-  Goal.list_map begin fun defs g ->
-    let (a,defs) = Goal.eval s env defs g in
-    (k a) , defs
-  end step.comb step.solution
-(* In form of a tactic *)
-let list_of_sensitive s k env =
-  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  let (>>) = Inner.seq in
-  Inner.get >>= fun step ->
-  try 
-    let (tacs,defs) = list_of_sensitive s k env step in
-    Inner.set { step with solution = defs; } >>
-    Inner.return tacs
-  with e when Errors.noncritical e ->
-    tclZERO e env
-
-let tclGOALBIND s k =
-  (* spiwack: the first line ensures that the value returned by the tactic [k] will
-      not "escape its scope". *)
-  let k a = tclBIND (k a) here_s in
-  tclBIND (list_of_sensitive s k) begin fun tacs ->
-    tclDISPATCHGEN Goal.null Goal.plus tacs
-  end
-
-let tclGOALBINDU s k =
-  tclBIND (list_of_sensitive s k) begin fun tacs ->
-    tclDISPATCHGEN () unitK tacs
-  end
 
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
@@ -427,21 +366,6 @@ let sensitive_on_proofview s env step =
   with e when Errors.noncritical e ->
     tclZERO e env
 
-(* spiwack: [lift_sensitive] is probably a better abstraction
-   than [tclGOALBIND]. *)
-let lift_sensitive s env =
-  (* spiwack: convenience notations, waiting for ocaml 3.12 *)
-  let (>>=) = Inner.bind in
-  let (>>) = Inner.seq in
-  Inner.get >>= fun step ->
-  let (res,sigma) =
-    Goal.list_map begin fun sigma g ->
-      Goal.eval s env step.solution g
-    end step.comb step.solution
-  in
-  Inner.set { step with solution=sigma } >>
-  Inner.return res
-
 (* arnaud: on pourrait regarder la liste de buts aussi, mais je
    ne sais pas encore comment. Pour l'instant on fait au plus
    simple. *)
@@ -499,13 +423,36 @@ let tclTIMEOUT n t g =
 let in_proofview p k =
   k p.solution
 
+
+(* spiwack: to help using `bind' like construct consistently. A glist
+   is promissed to have exactly one element per goal when it is
+   produced. *)
+type 'a glist  = 'a list
+
 module Notations = struct
   let (>-) = Goal.bind
-  let (>>-) = tclGOALBINDU
-  let (>>--) = tclGOALBIND
   let (>=) = tclBIND
-  let (>>=) t k = t >= fun s -> s >>- k
-  let (>>==) t k = t >= fun s -> s >>-- k
+  let (>>-) t k =
+    (* spiwack: the application of List.map may raise errors, as this
+       combinator is mostly used in porting historical tactic code,
+       where the error flow is somewhat hard to follow, hence the
+       try/with *)
+      t >= fun l ->
+      try tclDISPATCH (List.map k l)
+      with e when Errors.noncritical e -> tclZERO e
+  let (>>--) t k =
+    (* spiwack: the application of List.map may raise errors, as this
+       combinator is mostly used in porting historical tactic code,
+       where the error flow is somewhat hard to follow, hence the
+       try/with *)
+    begin
+      t >= fun l ->
+      try tclDISPATCHL (List.map k l)
+      with e when Errors.noncritical e -> tclZERO e
+    end >= fun l' ->
+    tclUNIT (List.flatten l')
+  let (>>=) = (>>-)
+  let (>>==) = (>>--)
   let (<*>) = tclTHEN
   let (<+>) = tclOR
 end
@@ -515,15 +462,8 @@ let rec list_map f = function
   | [] -> tclUNIT []
   | a::l ->
       f a >= fun a' ->
-      list_map f l >= fun l' ->
-      tclUNIT (a'::l')
-
-let rec sensitive_list_map f = function
-  | [] -> tclUNIT (Goal.return [])
-  | a::l ->
-      f a >>== fun a' ->
-      sensitive_list_map f l >>== fun l' ->
-      tclUNIT (Goal.return (a'::l'))
+        list_map f l >= fun l' ->
+          tclUNIT (a'::l')
 
 
 (*** Compatibility layer with <= 8.2 tactics ***)
@@ -600,12 +540,39 @@ module V82 = struct
 
   let of_tactic t gls =
     let init = { solution = gls.Evd.sigma ; comb = [gls.Evd.it] ; initial = [] } in
-    let final = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
+    let (_,final) = apply (Goal.V82.env gls.Evd.sigma gls.Evd.it) t init in
     { Evd.sigma = final.solution ; it = final.comb }
 
 end
 
 
+module Goal = struct
+
+  type 'a u = 'a list
+
+  let lift s env =
+    (* spiwack: convenience notations, waiting for ocaml 3.12 *)
+    let (>>=) = Inner.bind in
+    let (>>) = Inner.seq in
+    Inner.get >>= fun step ->
+    try
+      let (res,sigma) =
+        Goal.list_map begin fun sigma g ->
+          Goal.eval s env sigma g
+        end step.comb step.solution
+      in
+      Inner.set { step with solution=sigma } >>
+        Inner.return res
+    with e when Errors.noncritical e ->
+      tclZERO e env
+
+  let return x = lift (Goal.return x)
+  let concl = lift Goal.concl
+  let hyps = lift Goal.hyps
+  let env = lift Goal.env
+end
+
+
 
 
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 6165b02a9..93d1f2bb6 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -118,7 +118,7 @@ val unfocus : focus_context -> proofview -> proofview
 type +'a tactic 
 
 (* Applies a tactic to the current proofview. *)
-val apply : Environ.env -> 'a tactic -> proofview -> proofview
+val apply : Environ.env -> 'a tactic -> proofview -> 'a * proofview
 
 (*** tacticals ***)
 
@@ -167,9 +167,6 @@ val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
     sense in the goals immediatly built by it, and would cause an anomaly
     is used otherwise. *)
 val tclDISPATCH : unit tactic list -> unit tactic
-(* arnaud: quick hack to fix the order of goal solving to comply with Ltac.
-   it will probably have to go. *)
-val tclDISPATCHS : 'a Goal.sensitive tactic list -> 'a Goal.sensitive tactic
 val tclDISPATCHL : 'a tactic list -> 'a list tactic
 
 (* [tclEXTEND b r e] is a variant to [tclDISPATCH], where the [r] tactic
@@ -178,18 +175,9 @@ val tclDISPATCHL : 'a tactic list -> 'a list tactic
     is applied to every goal in between. *)
 val tclEXTEND : unit tactic list -> unit tactic -> unit tactic list -> unit tactic
 
-(* A sort of bind which takes a [Goal.sensitive] as a first argument, 
-    the tactic then acts on each goal separately.
-    Allows backtracking between goals. *)
-val tclGOALBIND : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
-val tclGOALBINDU : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
-
 (* [tclSENSITIVE] views goal-type tactics as a special kind of tactics.*)
 val tclSENSITIVE : Goal.subgoals Goal.sensitive -> unit tactic 
 
-(* [lift_sensitive s] returns the list corresponding to the evaluation
-   of [s] on each of the focused goals *)
-val lift_sensitive : 'a Goal.sensitive -> 'a list tactic
 
 (* [tclPROGRESS t] behaves has [t] as long as [t] progresses. *)
 val tclPROGRESS : 'a tactic -> 'a tactic
@@ -197,7 +185,10 @@ val tclPROGRESS : 'a tactic -> 'a tactic
 (* [tclEVARMAP] doesn't affect the proof, it returns the current evar_map. *)
 val tclEVARMAP : Evd.evar_map tactic
 
-(* [tclENV] doesn't affect the proof, it returns the current evar_map. *)
+(* [tclENV] doesn't affect the proof, it returns the current
+   environment.  It is not the environment of a particular goal,
+   rather the "global" environment of the proof. The goal-wise
+   environment is returned by {!Proofview.Goal.env}. *)
 val tclENV : Environ.env tactic
 
 (* [tclTIMEOUT n t] runs [t] for at most [n] seconds, succeeds if [t]
@@ -206,31 +197,36 @@ val tclENV : Environ.env tactic
 val tclTIMEOUT : int -> unit tactic -> unit tactic
 
 val list_map : ('a -> 'b tactic) -> 'a list -> 'b list tactic
-val sensitive_list_map : ('a -> 'b Goal.sensitive tactic) -> 'a list -> 'b list Goal.sensitive tactic
 
 (*** Commands ***)
 
 val in_proofview : proofview -> (Evd.evar_map -> 'a) -> 'a
 
+(* spiwack: to help using `bind' like construct consistently. A glist
+   is promissed to have exactly one element per goal when it is
+   produced. *)
+type 'a glist  = private 'a list
+
 (* Notations for building tactics. *)
 module Notations : sig
   (* Goal.bind *)
   val (>-) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive) -> 'b Goal.sensitive
-  (* tclGOALBINDU *)
-  val (>>-) : 'a Goal.sensitive -> ('a -> unit tactic) -> unit tactic
-  (* tclGOALBIND *)
-  val (>>--) : 'a Goal.sensitive -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+  (* [t >>- k] is [tclBIND t (fun l -> tclDISPATCH (List.map k l))] *)
+  val (>>-) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
+  (* arnaud: commenter *)
+  val (>>--) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
 
   (* tclBIND *)
   val (>=) : 'a tactic -> ('a -> 'b tactic) -> 'b tactic
 
+  (* arnaud: commentaire à mettre à jour *)
   (* [(>>=)] (and its goal sensitive variant [(>>==)]) "binds" in one step the
       tactic monad and the goal-sensitive monad.
       It is strongly advised to use it everytieme an ['a Goal.sensitive tactic]
       needs a bind, since it usually avoids to delay the interpretation of the
       goal sensitive value to a location where it does not make sense anymore. *)
-  val (>>=) : 'a Goal.sensitive tactic -> ('a -> unit tactic) -> unit tactic
-  val (>>==) : 'a Goal.sensitive tactic -> ('a -> 'b Goal.sensitive tactic) -> 'b Goal.sensitive tactic
+  val (>>=) : 'a glist tactic -> ('a -> unit tactic) -> unit tactic
+  val (>>==) : 'a glist tactic -> ('a -> 'b glist tactic) -> 'b glist tactic
 
   (* tclTHEN *)
   val (<*>) : unit tactic -> 'a tactic -> 'a tactic
@@ -238,6 +234,7 @@ module Notations : sig
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 end
 
+
 (*** Compatibility layer with <= 8.2 tactics ***)
 module V82 : sig
   type tac = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma 
@@ -267,3 +264,21 @@ module V82 : sig
      expected for a tactic obtained from {!V82.tactic} though. *)
   val of_tactic : 'a tactic -> tac
 end
+
+
+module Goal : sig
+
+  (* [lift_sensitive s] returns the list corresponding to the evaluation
+     of [s] on each of the focused goals *)
+  val lift : 'a Goal.sensitive -> 'a glist tactic
+  
+
+  (* [lift (Goal.return x)] *)
+  val return : 'a -> 'a glist tactic
+  (* [lift Goal.concl] *)    
+  val concl : Term.constr glist tactic
+  (* [lift Goal.hyps] *)
+  val hyps : Environ.named_context_val glist tactic
+  (* [lift Goal.env] *)
+  val env : Environ.env glist tactic
+end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d08dfd67d..a50c06b39 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -208,28 +208,37 @@ module New = struct
   open Proofview.Notations
 
   let pf_apply f =
-    Goal.env >- fun env ->
-    Goal.defs >- fun sigma ->
-    Goal.return (f env sigma)
+    Proofview.Goal.lift begin
+      Goal.env >- fun env ->
+      Goal.defs >- fun sigma ->
+      Goal.return (f env sigma)
+    end
 
   let of_old f =
-    Goal.V82.to_sensitive f
+    Proofview.Goal.lift (Goal.V82.to_sensitive f)
 
-  let pf_global id =
+  let pf_global_sensitive id =
     Goal.hyps >- fun hyps ->
     let hyps = Environ.named_context_of_val hyps in
     Goal.return (Constrintern.construct_reference hyps id)
 
-  let pf_ids_of_hyps =
+  let pf_global id =
+    Proofview.Goal.lift (pf_global_sensitive id)
+
+  let pf_ids_of_hyps_sensitive =
     Goal.hyps >- fun hyps ->
-      let hyps = Environ.named_context_of_val hyps in
-      Goal.return (ids_of_named_context hyps)
+    let hyps = Environ.named_context_of_val hyps in
+    Goal.return (ids_of_named_context hyps)
+  let pf_ids_of_hyps =
+    Proofview.Goal.lift pf_ids_of_hyps_sensitive
 
   let pf_get_new_id id =
-    pf_ids_of_hyps >- fun ids ->
-    Goal.return (next_ident_away id ids)
+    Proofview.Goal.lift begin
+      pf_ids_of_hyps_sensitive >- fun ids ->
+      Goal.return (next_ident_away id ids)
+    end
 
-  let pf_get_hyp id =
+  let pf_get_hyp_sensitive id =
     Goal.hyps >- fun hyps ->
     let hyps = Environ.named_context_of_val hyps in
     let sign =
@@ -237,18 +246,26 @@ module New = struct
       with Not_found -> Errors.error ("No such hypothesis: " ^ (string_of_id id))
     in
     Goal.return sign
+  let pf_get_hyp id =
+    Proofview.Goal.lift (pf_get_hyp_sensitive id)
 
-  let pf_get_hyp_typ id =
-    pf_get_hyp id >- fun (_,_,ty) ->
+  let pf_get_hyp_typ_sensitive id =
+    pf_get_hyp_sensitive id >- fun (_,_,ty) ->
     Goal.return ty
+  let pf_get_hyp_typ id =
+    Proofview.Goal.lift (pf_get_hyp_typ_sensitive id)
 
   let pf_hyps_types =
-    Goal.env >- fun env ->
-    let sign = Environ.named_context env in
-    Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+    Proofview.Goal.lift begin
+      Goal.env >- fun env ->
+      let sign = Environ.named_context env in
+      Goal.return (List.map (fun (id,_,x) -> (id, x)) sign)
+    end
 
   let pf_last_hyp =
-    Goal.hyps >- fun hyps ->
-    Goal.return (List.hd (Environ.named_context_of_val hyps))
+    Proofview.Goal.lift begin
+      Goal.hyps >- fun hyps ->
+      Goal.return (List.hd (Environ.named_context_of_val hyps))
+    end
 
 end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index b3e442abc..7c96bd93b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,19 +134,29 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
+  open Goal
+  open Proofview
+
+  val pf_apply : (env -> evar_map -> 'a) -> 'a glist tactic
+  val pf_global_sensitive : identifier -> constr sensitive
+  val pf_global : identifier -> constr glist tactic
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a glist tactic
+
+  val pf_get_new_id  : identifier -> identifier glist tactic
+  val pf_ids_of_hyps_sensitive : identifier list sensitive
+  val pf_ids_of_hyps : identifier list glist tactic
+  val pf_hyps_types : (identifier * types) list glist tactic
+
+  val pf_get_hyp_sensitive : identifier -> named_declaration sensitive
+  val pf_get_hyp : identifier -> named_declaration glist tactic
+  val pf_get_hyp_typ_sensitive : identifier -> types sensitive
+  val pf_get_hyp_typ        : identifier -> types glist tactic
+  val pf_last_hyp           : named_declaration glist tactic
+end
+
 
-  val pf_apply : (env -> evar_map -> 'a) -> 'a Goal.sensitive
-  val pf_global : identifier -> constr Goal.sensitive
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> 'a Goal.sensitive
 
-  val pf_get_new_id  : identifier -> identifier Goal.sensitive
-  val pf_ids_of_hyps : identifier list Goal.sensitive
-  val pf_hyps_types : (identifier * types) list Goal.sensitive
 
-  val pf_get_hyp : identifier -> named_declaration Goal.sensitive
-  val pf_get_hyp_typ        : identifier -> types Goal.sensitive
-  val pf_last_hyp           : named_declaration Goal.sensitive
-end