Indexing Proofview.goals with a stage.

This is not perfect though, some primitives are unsound, and some
higher-order API should use polymorphic functions so as not to depend
on a given level.

12 files changed, 109 insertions, 87 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a0e61623c7..470e21c820 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -888,7 +888,7 @@ struct
 
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.New.pf_env gl) (Goal.sigma gl) t1 t2
+   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
 
   let parse_zop gl (op,args) =
    match kind_of_term op with
@@ -1169,8 +1169,8 @@ struct
       with e when Errors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-     let ty   = Typing.unsafe_type_of (Goal.env gl) (Goal.sigma gl) term in
-     let sort = Typing.sort_of (Goal.env gl) (ref (Goal.sigma gl)) ty in
+     let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
+     let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
      Term.is_prop_sort sort in
      
     let rec xparse_formula env tg term =
@@ -1446,6 +1446,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let vm = dump_varmap (spec.typ) env in
  (* todo : directly generate the proof term - or generalize before conversion? *)
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
+   let gl = Tacmach.New.of_old (fun x -> x) gl in
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1457,7 +1458,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
 	[["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.New.pf_concl gl))
+      (Tacmach.pf_concl gl))
    ;
    Tactics.new_generalize env ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
@@ -1708,8 +1709,9 @@ let micromega_gen
     unsat deduce 
     spec prover =
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
-    let concl = Tacmach.New.pf_concl gl in
-    let hyps  = Tacmach.New.pf_hyps_types gl in
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
+    let concl = Tacmach.pf_concl gl in
+    let hyps  = Tacmach.pf_hyps_types gl in
     try
      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
      let env = Env.elements env in
@@ -1755,6 +1757,7 @@ let micromega_order_changer cert env ff  =
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -1766,7 +1769,7 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.New.pf_concl gl)));
+        (Tacmach.pf_concl gl)));
       Tactics.new_generalize env ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
@@ -1787,8 +1790,9 @@ let micromega_genr prover =
     dump_proof = dump_psatz coq_Q dump_q
   } in
   Proofview.Goal.nf_enter { enter = begin fun gl -> 
-     let concl = Tacmach.New.pf_concl gl in
-     let hyps  = Tacmach.New.pf_hyps_types gl in
+     let gl = Tacmach.New.of_old (fun x -> x) gl in
+     let concl = Tacmach.pf_concl gl in
+     let hyps  = Tacmach.pf_hyps_types gl in
      try
       let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
        let env = Env.elements env in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index b8a58daeb2..826b4772a0 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -908,17 +908,17 @@ let catchable_exception = function
 
 module Goal = struct
 
-  type 'a t = {
+  type ('a, 'r) t = {
     env : Environ.env;
     sigma : Evd.evar_map;
     concl : Term.constr ;
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  type 'a enter =
-    { enter : 'a t -> unit tactic }
+  type ('a, 'b) enter =
+    { enter : 'r. ('a, 'r) t -> 'b }
 
-  let assume (gl : 'a t) = (gl :> [ `NF ] t)
+  let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
 
   let env { env=env } = env
   let sigma { sigma=sigma } = sigma
@@ -977,8 +977,8 @@ module Goal = struct
     end
     end
 
-  type 'a s_enter =
-    { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type ('a, 'b) s_enter =
+    { s_enter : 'r. ('a, 'r) t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma }
 
   let s_enter f =
     InfoL.tag (Info.Dispatch) begin
@@ -1033,6 +1033,8 @@ module Goal = struct
   (* compatibility *)
   let goal { self=self } = self
 
+  let lift (gl : ('a, 'r) t) _ = (gl :> ('a, 's) t)
+
 end
 
 
@@ -1257,8 +1259,8 @@ module Notations = struct
   let (>>=) = tclBIND
   let (<*>) = tclTHEN
   let (<+>) t1 t2 = tclOR t1 (fun _ -> t2)
-  type 'a enter = 'a Goal.enter =
-    { enter : 'a Goal.t -> unit tactic }
-  type 'a s_enter = 'a Goal.s_enter =
-    { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type ('a, 'b) enter = ('a, 'b) Goal.enter =
+    { enter : 'r. ('a, 'r) Goal.t -> 'b }
+  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
+    { s_enter : 'r. ('a, 'r) Goal.t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma }
 end
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 1616782e54..5c97ada344 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -418,61 +418,71 @@ end
 
 module Goal : sig
 
-  (** The type of goals. The parameter type is a phantom argument indicating
-      whether the data contained in the goal has been normalized w.r.t. the
-      current sigma. If it is the case, it is flagged [ `NF ]. You may still
-      access the un-normalized data using {!assume} if you known you do not rely
-      on the assumption of being normalized, at your own risk. *)
-  type 'a t
+  (** Type of goals.
+
+      The first parameter type is a phantom argument indicating whether the data
+      contained in the goal has been normalized w.r.t. the current sigma. If it
+      is the case, it is flagged [ `NF ]. You may still access the un-normalized
+      data using {!assume} if you known you do not rely on the assumption of
+      being normalized, at your own risk.
+
+      The second parameter is a stage indicating where the goal belongs. See
+      module {!Sigma}.
+  *)
+  type ('a, 'r) t
 
   (** Assume that you do not need the goal to be normalized. *)
-  val assume : 'a t -> [ `NF ] t
+  val assume : ('a, 'r) t -> ([ `NF ], 'r) t
 
   (** Normalises the argument goal. *)
-  val normalize : 'a t -> [ `NF ] t tactic
+  val normalize : ('a, 'r) t -> ([ `NF ], 'r) t tactic
 
   (** [concl], [hyps], [env] and [sigma] given a goal [gl] return
       respectively the conclusion of [gl], the hypotheses of [gl], the
       environment of [gl] (i.e. the global environment and the
       hypotheses) and the current evar map. *)
-  val concl : [ `NF ] t -> Term.constr
-  val hyps : [ `NF ] t -> Context.named_context
-  val env : 'a t -> Environ.env
-  val sigma : 'a t -> Evd.evar_map
-  val extra : 'a t -> Evd.Store.t
+  val concl : ([ `NF ], 'r) t -> Term.constr
+  val hyps : ([ `NF ], 'r) t -> Context.named_context
+  val env : ('a, 'r) t -> Environ.env
+  val sigma : ('a, 'r) t -> Evd.evar_map
+  val extra : ('a, 'r) t -> Evd.Store.t
 
   (** Returns the goal's conclusion even if the goal is not
       normalised. *)
-  val raw_concl : 'a t -> Term.constr
+  val raw_concl : ('a, 'r) t -> Term.constr
 
-  type 'a enter =
-    { enter : 'a t -> unit tactic }
+  type ('a, 'b) enter =
+    { enter : 'r. ('a, 'r) t -> 'b }
 
   (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
       independently, in the manner of {!tclINDEPENDENT} except that
       the current goal is also given as an argument to [t]. The goal
       is normalised with respect to evars. *)
-  val nf_enter : [ `NF ] enter -> unit tactic
+  val nf_enter : ([ `NF ], unit tactic) enter -> unit tactic
 
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : [ `LZ ] enter -> unit tactic
+  val enter : ([ `LZ ], unit tactic) enter -> unit tactic
 
-  type 'a s_enter =
-    { s_enter : 'r. 'a t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type ('a, 'b) s_enter =
+    { s_enter : 'r. ('a, 'r) t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma }
 
   (** A variant of {!enter} allows to work with a monotonic state. The evarmap
       returned by the argument is put back into the current state before firing
       the returned tactic. *)
-  val s_enter : [ `LZ ] s_enter -> unit tactic
+  val s_enter : ([ `LZ ], unit tactic) s_enter -> unit tactic
 
   (** Like {!s_enter}, but normalizes the goal beforehand. *)
-  val nf_s_enter : [ `NF ] s_enter -> unit tactic
+  val nf_s_enter : ([ `NF ], unit tactic) s_enter -> unit tactic
 
-  (** Recover the list of current goals under focus, without evar-normalization *)
-  val goals : [ `LZ ] t tactic list tactic
+  (** Recover the list of current goals under focus, without evar-normalization.
+      FIXME: encapsulate the level in an existential type. *)
+  val goals : ([ `LZ ], 'r) t tactic list tactic
 
   (** Compatibility: avoid if possible *)
-  val goal : [ `NF ] t -> Evar.t
+  val goal : ([ `NF ], 'r) t -> Evar.t
+
+  (** Every goal is valid at a later stage. FIXME: take a later evarmap *)
+  val lift : ('a, 'r) t -> ('r, 's) Sigma.le -> ('a, 's) t
 
 end
 
@@ -595,8 +605,8 @@ module Notations : sig
   (** {!tclOR}: [t1+t2] = [tclOR t1 (fun _ -> t2)]. *)
   val (<+>) : 'a tactic -> 'a tactic -> 'a tactic
 
-  type 'a enter = 'a Goal.enter =
-    { enter : 'a Goal.t -> unit tactic }
-  type 'a s_enter = 'a Goal.s_enter =
-    { s_enter : 'r. 'a Goal.t -> 'r Sigma.t -> (unit tactic, 'r) Sigma.sigma }
+  type ('a, 'b) enter = ('a, 'b) Goal.enter =
+    { enter : 'r. ('a, 'r) Goal.t -> 'b }
+  type ('a, 'b) s_enter = ('a, 'b) Goal.s_enter =
+    { s_enter : 'r. ('a, 'r) Goal.t -> 'r Sigma.t -> ('b, 'r) Sigma.sigma }
 end
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 4238d1e372..8af28b6ab1 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -212,7 +212,7 @@ module New = struct
     let hyps = Proofview.Goal.hyps gl in
     List.hd hyps
 
-  let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) =
+  let pf_nf_concl (gl : ([ `LZ ], 'r) Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a0e1a01577..3ed6a2eeb1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -106,36 +106,37 @@ val pr_glls   : goal list sigma -> Pp.std_ppcmds
 
 (* Variants of [Tacmach] functions built with the new proof engine *)
 module New : sig
-  val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a
-  val pf_global : identifier -> 'a Proofview.Goal.t -> constr
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
+  val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a
+  val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr
+  (** FIXME: encapsulate the level in an existential type. *)
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
 
-  val pf_env : 'a Proofview.Goal.t -> Environ.env
-  val pf_concl : [ `NF ] Proofview.Goal.t -> types
+  val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
+  val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
 
-  val pf_unsafe_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
-  val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> evar_map * Term.types
-  val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
+  val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> Term.constr -> evar_map * Term.types
+  val pf_conv_x : ('a, 'r) Proofview.Goal.t -> Term.constr -> Term.constr -> bool
 
-  val pf_get_new_id  : identifier -> [ `NF ] Proofview.Goal.t -> identifier
-  val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
-  val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
+  val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier
+  val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
+  val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : identifier -> [ `NF ] Proofview.Goal.t -> types
-  val pf_last_hyp           : [ `NF ] Proofview.Goal.t -> named_declaration
+  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
+  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
 
-  val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types
-  val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> pinductive * types
+  val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types
 
-  val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types
-  val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
+  val pf_hnf_constr : ('a, 'r) Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types
 
-  val pf_whd_betadeltaiota : 'a Proofview.Goal.t -> constr -> constr
-  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
+  val pf_whd_betadeltaiota : ('a, 'r) Proofview.Goal.t -> constr -> constr
+  val pf_compute : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
-  val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
+  val pf_matches : ('a, 'r) Proofview.Goal.t -> constr_pattern -> constr -> patvar_map
 
-  val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
+  val pf_nf_evar : ('a, 'r) Proofview.Goal.t -> constr -> constr
 
 end
diff --git a/tactics/auto.mli b/tactics/auto.mli
index cae180ce76..215544a591 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -26,7 +26,7 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-			 [ `NF ] Proofview.Goal.t -> clausenv * constr
+			 ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr
 						
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve_nodelta : polymorphic -> (raw_hint * clausenv) -> unit Proofview.tactic
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9c22beba27..8ee3ec9281 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -166,15 +166,17 @@ let e_give_exact flags poly (c,clenv) gl =
   let t1 = pf_unsafe_type_of gl c in
     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
-let unify_e_resolve poly flags (c,clenv) gls =
+let unify_e_resolve poly flags = { enter = begin fun gls (c,clenv) ->
   let clenv', c = connect_hint_clenv poly c clenv gls in
   let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
     Clenvtac.clenv_refine true ~with_classes:false clenv'
+  end }
 
-let unify_resolve poly flags (c,clenv) gls =
+let unify_resolve poly flags = { enter = begin fun gls (c,clenv) ->
   let clenv', _ = connect_hint_clenv poly c clenv gls in
   let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
     Clenvtac.clenv_refine false ~with_classes:false clenv'
+  end }
 
 let clenv_of_prods poly nprods (c, clenv) gl =
   let (c, _, _) = c in
@@ -191,7 +193,7 @@ let with_prods nprods poly (c, clenv) f =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   match clenv_of_prods poly nprods (c, clenv) gl with
   | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
-  | Some clenv' -> f (c, clenv') gl
+  | Some clenv' -> f.enter gl (c, clenv')
   end }
 
 (** Hack to properly solve dependent evars that are typeclasses *)
@@ -902,5 +904,5 @@ let autoapply c i gl =
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
   let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let tac = { enter = fun gl -> unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) gl } in
+  let tac = { enter = fun gl -> (unify_e_resolve false flags).enter gl ((c,cty,Univ.ContextSet.empty),ce) } in
   Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e8f88fca10..0c487c4e63 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1795,6 +1795,7 @@ let rewrite_assumption_cond cond_eq_term cl =
 	end
   in
   Proofview.Goal.nf_enter { enter = begin fun gl ->
+    let gl = Proofview.Goal.lift gl Sigma.Unsafe.le in
     let hyps = Proofview.Goal.hyps gl in
     arec hyps gl
   end }
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index 4835156748..4496499229 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -37,12 +37,14 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
 
 (** {5 Focussing} *)
 
-val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
+val nf_enter : (([ `NF ], 'r) Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal. The resulting tactic is focussed. *)
+(** FIXME: Should be polymorphic over the stage. *)
 
-val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
+val enter : (([ `LZ ], 'r) Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal, without evar normalization. The resulting tactic is
     focussed. *)
+(** FIXME: Should be polymorphic over the stage. *)
 
 val with_env : 'a t -> (Environ.env*'a) t
 (** [with_env t] returns, in addition to the return type of [t], an
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 27d25056e1..281e6b9bb9 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -119,11 +119,11 @@ val match_with_equation:
 
 (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] 
    Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *)
-val find_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : [ `NF ] Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr ->
       coq_eq_data * Univ.universe_instance * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
@@ -144,7 +144,7 @@ val is_matching_sigma : constr -> bool
 val match_eqdec : constr -> bool * constr * constr * constr * constr
 
 (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
-val dest_nf_eq : [ `NF ] Proofview.Goal.t -> constr -> (constr * constr * constr)
+val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr)
 
 (** Match a negation *)
 val is_matching_not : constr -> bool
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 3c56bbdc0d..c67053252b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -560,7 +560,7 @@ module New = struct
       tac2 id
     end }
 
-  let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find gl) end }
+  let onHyps find tac = Proofview.Goal.nf_enter { enter = begin fun gl -> tac (find.enter gl) end }
 
   let afterHyp id tac =
     Proofview.Goal.nf_enter { enter = begin fun gl ->
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4e860892d0..80e01a8d07 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -223,7 +223,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : [ `NF ] Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -234,7 +234,7 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `NF ] Proofview.Goal.t -> named_context) ->
+  val onHyps      : ([ `NF ], named_context) Proofview.Goal.enter ->
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
@@ -242,9 +242,9 @@ module New : sig
   val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
   val onClause   : (identifier option -> unit tactic) -> clause -> unit tactic
 
-  val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_hyp  : Id.t -> 'a Proofview.Goal.t -> sorts_family
-  val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_goal : ('a, 'r) Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_hyp  : Id.t -> ('a, 'r) Proofview.Goal.t -> sorts_family
+  val elimination_sort_of_clause : Id.t option -> ('a, 'r) Proofview.Goal.t -> sorts_family
 
   val elimination_then :
     (branch_args -> unit Proofview.tactic) ->