[engine] Remove ghost parameter from `Proofview.Goal.t`

In current code, `Proofview.Goal.t` uses a phantom type to indicate
whether the goal was properly substituted wrt current `evar_map` or
not.

After the introduction of `EConstr`, this distinction should have
become unnecessary, thus we remove the phantom parameter from
`'a Proofview.Goal.t`. This may introduce some minor incompatibilities
at the typing level. Code-wise, things should remain the same.

We thus deprecate `assume`. In a next commit, we will remove
normalization as much as possible from the code.

28 files changed, 112 insertions, 128 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index aef62b009..16a31790a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -20,6 +20,14 @@ General deprecation
   removed. Please, make sure your plugin is warning-free in 8.7 before
   trying to port it over 8.8.
 
+Proof engine
+
+  Due to the introduction of `EConstr` in 8.7, it is not necessary to
+  track "goal evar normal form status" anymore, thus the type `'a
+  Proofview.Goal.t` loses its ghost argument. This may introduce some
+  minor incompatibilities at the typing level. Code-wise, things
+  should remain the same.
+
 We removed the following functions:
 
 - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context`
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index c108c0c2e..65ee929c8 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -39,10 +39,10 @@ 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 : (Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal. The resulting tactic is focussed. *)
 
-val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
+val enter : (Proofview.Goal.t -> 'a t) -> 'a t
 (** Enter a goal, without evar normalization. The resulting tactic is
     focussed. *)
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 47b9b406d..c41b0b0dc 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -1023,14 +1023,14 @@ let catchable_exception = function
 
 module Goal = struct
 
-  type 'a t = {
+  type t = {
     env : Environ.env;
     sigma : Evd.evar_map;
     concl : EConstr.constr ;
     self : Evar.t ; (* for compatibility with old-style definitions *)
   }
 
-  let assume (gl : 'a t) = (gl :> [ `NF ] t)
+  let assume (gl : t) = (gl : t)
 
   let env {env} = env
   let sigma {sigma} = sigma
diff --git a/engine/proofview.mli b/engine/proofview.mli
index b02fde3a8..721ce507d 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -461,56 +461,49 @@ end
 
 module Goal : sig
 
-  (** 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.
-
-  *)
-  type 'a t
+  (** Type of goals. *)
+  type t
 
   (** Assume that you do not need the goal to be normalized. *)
-  val assume : 'a t -> [ `NF ] t
+  val assume : t -> t
+  [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"]
 
   (** Normalises the argument goal. *)
-  val normalize : 'a t -> [ `NF ] t tactic
+  val normalize : t -> 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 : 'a t -> constr
-  val hyps : 'a t -> named_context
-  val env : 'a t -> Environ.env
-  val sigma : 'a t -> Evd.evar_map
-  val extra : 'a t -> Evd.Store.t
+  val concl : t -> constr
+  val hyps : t -> named_context
+  val env : t -> Environ.env
+  val sigma : t -> Evd.evar_map
+  val extra : t -> Evd.Store.t
 
   (** [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 ] t -> unit tactic) -> unit tactic
+  val nf_enter : (t -> unit tactic) -> unit tactic
 
   (** Like {!nf_enter}, but does not normalize the goal beforehand. *)
-  val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
+  val enter : (t -> unit tactic) -> unit tactic
 
   (** Like {!enter}, but assumes exactly one goal under focus, raising *)
   (** a fatal error otherwise. *)
-  val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic
+  val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic
 
   (** Recover the list of current goals under focus, without evar-normalization.
       FIXME: encapsulate the level in an existential type. *)
-  val goals : [ `LZ ] t tactic list tactic
+  val goals : t tactic list tactic
 
   (** [unsolved g] is [true] if [g] is still unsolved in the current
       proof state. *)
-  val unsolved : 'a t -> bool tactic
+  val unsolved : t -> bool tactic
 
   (** Compatibility: avoid if possible *)
-  val goal : [ `NF ] t -> Evar.t
+  val goal : t -> Evar.t
 
 end
 
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index 9742a002d..01138702b 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -138,7 +138,6 @@ let declare_tactic_argument loc s (typ, f, g, h) cl =
       <:expr<
         let f = $lid:f$ in
         fun ist v -> Ftactic.enter (fun gl ->
-          let gl = Proofview.Goal.assume gl in
           let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in
           let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in
           Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v)
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 8642df684..7f8f60e46 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -187,7 +187,7 @@ let make_prb gls depth additionnal_terms =
   let open Tacmach.New in
   let env=pf_env gls in
   let sigma=project gls in
-  let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in
+  let state = empty depth {it = Proofview.Goal.goal gls; sigma } in
   let pos_hyps = ref [] in
   let neg_hyps =ref [] in
     List.iter
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d46201335..09147d606 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -37,7 +37,7 @@ let ground_tac solver startseq =
     let () =
       if Tacinterp.get_debug()=Tactic_debug.DebugOn 0
       then
-        let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in
+        let gl = { Evd.it = Proofview.Goal.goal gl; sigma = project gl } in
         Feedback.msg_debug (Printer.pr_goal gl)
     in
     tclORELSE (axiom_tac seq.gl seq)
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 0d491d92b..0f5417e7d 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -223,7 +223,7 @@ let mk_N = function
 
 module type Int = sig
   val typ : constr Lazy.t
-  val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool
+  val is_int_typ : Proofview.Goal.t -> constr -> bool
   val plus : constr Lazy.t
   val mult : constr Lazy.t
   val opp : constr Lazy.t
@@ -231,7 +231,7 @@ module type Int = sig
 
   val mk : Bigint.bigint -> constr
   val parse_term : constr -> parse_term
-  val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel
+  val parse_rel : Proofview.Goal.t -> constr -> parse_rel
   (* check whether t is built only with numbers and + * - *)
   val get_scalar : constr -> Bigint.bigint option
 end
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 5ba063d9d..ecddc55de 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -105,7 +105,7 @@ module type Int =
     (* the coq type of the numbers *)
     val typ : constr Lazy.t
     (* Is a constr expands to the type of these numbers *)
-    val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool
+    val is_int_typ : Proofview.Goal.t -> constr -> bool
     (* the operations on the numbers *)
     val plus : constr Lazy.t
     val mult : constr Lazy.t
@@ -116,7 +116,7 @@ module type Int =
     (* parsing a term (one level, except if a number is found) *)
     val parse_term : constr -> parse_term
     (* parsing a relation expression, including = < <= >= > *)
-    val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel
+    val parse_rel : Proofview.Goal.t -> constr -> parse_rel
     (* Is a particular term only made of numbers and + * - ? *)
     val get_scalar : constr -> Bigint.bigint option
   end
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 7cdf05117..5c06cf426 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1061,7 +1061,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
 (** Basic tactics *)
 
 let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl ->
-  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+  let concl = Proofview.Goal.concl gl in
   match EConstr.kind (Proofview.Goal.sigma gl) concl with
   | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
   | _ -> if red then Tacticals.New.tclZEROMSG (str"No product even after head-reduction.")
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 9a2026dd3..c894b9dc9 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -41,10 +41,10 @@ val clenv_nf_meta   : clausenv -> EConstr.constr -> EConstr.constr
 (** type of a meta in clenv context *)
 val clenv_meta_type : clausenv -> metavariable -> types
 
-val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv
 val mk_clenv_from_n :
-  'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
-val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv
+  Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv
+val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv
 val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv
 
 (** Refresh the universes in a clenv *)
@@ -66,7 +66,7 @@ val old_clenv_unique_resolver :
   ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
 val clenv_unique_resolver :
-  ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv
+  ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv
 
 val clenv_dependent : clausenv -> metavariable list
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8bd5d98cb..373d60e69 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -141,7 +141,7 @@ let fail_quick_unif_flags = {
 let unify ?(flags=fail_quick_unif_flags) m =
   Proofview.Goal.enter begin fun gl ->
     let env = Tacmach.New.pf_env gl in
-    let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
+    let n = Tacmach.New.pf_concl gl in
     let evd = clear_metas (Tacmach.New.project gl) in
     try
       let evd' = w_unify env evd CONV ~flags m n in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e3f650848..90276951b 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -70,7 +70,6 @@ let add_side_effects env effects =
   List.fold_left (fun env eff -> add_side_effect env eff) env effects
 
 let generic_refine ~typecheck f gl =
-  let gl = Proofview.Goal.assume gl in
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let concl = Proofview.Goal.concl gl in
@@ -159,7 +158,6 @@ let with_type env evd c t =
   evd , j'.Environ.uj_val
 
 let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl ->
-  let gl = Proofview.Goal.assume gl in
   let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
   let f h =
diff --git a/proofs/refine.mli b/proofs/refine.mli
index cfdcde36e..1932a306c 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -33,7 +33,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr
 (** A variant of [refine] which assumes exactly one goal under focus *)
 
 val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic ->
-  [ `NF ] Proofview.Goal.t -> 'a tactic
+  Proofview.Goal.t -> 'a tactic
 (** The general version of refine. *)
 
 (** {7 Helper functions} *)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index bdcb4868b..d3405b892 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -150,7 +150,6 @@ module New = struct
 
   let pf_global id gl =
     (** We only check for the existence of an [id] in [hyps] *)
-    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     Constrintern.construct_reference hyps id
 
@@ -167,13 +166,11 @@ module New = struct
 
   let pf_ids_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
-    let gl = Proofview.Goal.assume gl in
     let hyps = Proofview.Goal.hyps gl in
     ids_of_named_context hyps
 
   let pf_ids_set_of_hyps gl =
     (** We only get the identifiers in [hyps] *)
-    let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
     Environ.ids_of_named_context_val (Environ.named_context_val env)
 
@@ -204,9 +201,8 @@ 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 : Proofview.Goal.t) =
     (** We normalize the conclusion just after *)
-    let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = project gl in
     nf_evar sigma concl
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index e0fb8fbc5..8f69358d4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -92,46 +92,46 @@ val pr_glls   : goal list sigma -> Pp.t
 
 (* 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 : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference
+  val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
+  val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference
   (** FIXME: encapsulate the level in an existential type. *)
-  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
+  val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
 
-  val project : 'a Proofview.Goal.t -> Evd.evar_map
-  val pf_env : 'a Proofview.Goal.t -> Environ.env
-  val pf_concl : 'a Proofview.Goal.t -> types
+  val project : Proofview.Goal.t -> Evd.evar_map
+  val pf_env : Proofview.Goal.t -> Environ.env
+  val pf_concl : Proofview.Goal.t -> types
 
   (** WRONG: To be avoided at all costs, it typechecks the term entirely but
      forgets the universe constraints necessary to retypecheck it *)
-  val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types
+  val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types
 
   (** This function does no type inference and expects an already well-typed term.
       It recomputes its type in the fastest way possible (no conversion is ever involved) *)
-  val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types
+  val pf_get_type_of : Proofview.Goal.t -> constr -> types
 
   (** This function entirely type-checks the term and computes its type
       and the implied universe constraints. *)
-  val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types
-  val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool
+  val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types
+  val pf_conv_x : Proofview.Goal.t -> t -> t -> bool
 
-  val pf_get_new_id  : Id.t -> 'a Proofview.Goal.t -> Id.t
-  val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list
-  val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t
-  val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list
+  val pf_get_new_id  : Id.t -> Proofview.Goal.t -> Id.t
+  val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list
+  val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t
+  val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list
 
-  val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration
-  val pf_get_hyp_typ        : Id.t -> 'a Proofview.Goal.t -> types
-  val pf_last_hyp           : 'a Proofview.Goal.t -> named_declaration
+  val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration
+  val pf_get_hyp_typ        : Id.t -> Proofview.Goal.t -> types
+  val pf_last_hyp           : 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 -> (inductive * EInstance.t) * types
+  val pf_nf_concl : Proofview.Goal.t -> types
+  val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * 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 : Proofview.Goal.t -> constr -> types
+  val pf_hnf_type_of : Proofview.Goal.t -> constr -> types
 
-  val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr
-  val pf_compute : 'a Proofview.Goal.t -> constr -> constr
+  val pf_whd_all : Proofview.Goal.t -> constr -> constr
+  val pf_compute : Proofview.Goal.t -> constr -> constr
 
-  val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr
+  val pf_nf_evar : Proofview.Goal.t -> constr -> constr
 
 end
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e7e21b5f4..eec7a5f2a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -32,7 +32,7 @@ open Hints
 let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
 
 let compute_secvars gl =
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let hyps = Proofview.Goal.hyps gl in
   secvars_of_hyps hyps
 
 (* tell auto not to reuse already instantiated metas in unification (for
@@ -316,7 +316,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
           let sigma = Tacmach.New.project gl in
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
-          let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
+          let decl = Tacmach.New.pf_last_hyp gl in
           let hyp = Context.Named.Declaration.map_constr nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
diff --git a/tactics/auto.mli b/tactics/auto.mli
index b9cd4932c..59809331e 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -16,14 +16,14 @@ open Decl_kinds
 open Hints
 open Tactypes
 
-val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t
+val compute_secvars : Proofview.Goal.t -> Id.Pred.t
 
 val default_search_depth : int ref
 
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  'a Proofview.Goal.t -> clausenv * constr
+  Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index cfadfc535..a95e6b941 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -996,7 +996,7 @@ module Search = struct
              Hint_db.transparent_state cached_hints == st
     then cached_hints
     else
-      let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g}
+      let hints = make_hints {it = Goal.goal g; sigma = project g}
                              st only_classes sign
       in
       autogoal_cache := (cwd, only_classes, sign, hints); hints
@@ -1041,7 +1041,6 @@ module Search = struct
 
   let fail_if_nonclass info =
     Proofview.Goal.enter begin fun gl ->
-      let gl = Proofview.Goal.assume gl in
       let sigma = Proofview.Goal.sigma gl in
       if is_class_type sigma (Proofview.Goal.concl gl) then
         Proofview.tclUNIT ()
@@ -1089,7 +1088,7 @@ module Search = struct
             pr_depth (idx :: info.search_depth) ++ str": " ++
               Lazy.force pp ++
               (if !foundone != true then
-                 str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl))
+                 str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl)
                else mt ())
           in
           let msg =
@@ -1110,7 +1109,7 @@ module Search = struct
         if !typeclasses_debug > 0 then
           Feedback.msg_debug
             (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++
-               pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl')));
+               pr_ev sigma' (Proofview.Goal.goal gl'));
         let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in
         let hints' =
           if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl))
@@ -1119,7 +1118,7 @@ module Search = struct
             make_autogoal_hints info.search_only_classes ~st gl'
           else info.search_hints
         in
-        let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in
+        let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in
         let info' =
           { search_depth = succ j :: i :: info.search_depth;
             last_tac = pp;
@@ -1136,7 +1135,7 @@ module Search = struct
         (if !typeclasses_debug > 0 then
            Feedback.msg_debug
              (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp
-              ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl))
+              ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl)
               ++ str", " ++ int j ++ str" subgoal(s)" ++
                 (Option.cata (fun k -> str " in addition to the first " ++ int k)
                              (mt()) k)));
@@ -1261,7 +1260,7 @@ module Search = struct
     if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then
       Tacticals.New.tclZEROMSG (str"Not a subgoal for a class")
     else
-      let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in
+      let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in
       let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in
       search_tac hints depth 1 info
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 5e2006ccc..467754a84 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -53,7 +53,7 @@ let filter_hyp f tac =
     | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d)
     | _::rest -> seek rest in
   Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let hyps = Proofview.Goal.hyps gl in
     seek hyps
   end
 
@@ -98,7 +98,7 @@ let contradiction_context =
                  end)
 	  | _ -> seek_neg rest
     in
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let hyps = Proofview.Goal.hyps gl in
     seek_neg hyps
   end
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 6ea6155e0..785d2f515 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -32,7 +32,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state
 let e_give_exact ?(flags=eauto_unif_flags) c =
   Proofview.Goal.enter begin fun gl ->
   let t1 = Tacmach.New.pf_unsafe_type_of gl c in
-  let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
+  let t2 = Tacmach.New.pf_concl gl in
   let sigma = Tacmach.New.project gl in
   if occur_existential sigma t1 || occur_existential sigma t2 then
      Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 450d68436..674d01777 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -266,7 +266,7 @@ let rewrite_elim with_evars frzevars cls c e =
   end
 
 let tclNOTSAMEGOAL tac =
-  let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in
+  let goal gl = Proofview.Goal.goal gl in
   Proofview.Goal.nf_enter begin fun gl ->
     let sigma = project gl in
     let ev = goal gl in
@@ -324,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
     in
     let typ = match cls with
     | None -> pf_concl gl
-    | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl)
+    | Some id -> pf_get_hyp_typ id gl
     in
     let cs = instantiate_lemma typ in
     if firstonly then tclFIRST (List.map try_clause cs)
@@ -970,7 +970,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function
 let gen_absurdity id =
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
-  let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
+  let hyp_typ = pf_get_hyp_typ id gl in
   if is_empty_type sigma hyp_typ
   then
     simplest_elim (mkVar id)
@@ -1443,7 +1443,7 @@ let get_previous_hyp_position id gl =
     let hyp = Context.Named.Declaration.get_id d in
     if Id.equal hyp id then dest else aux (MoveAfter hyp) right
   in
-  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+  aux MoveLast (Proofview.Goal.hyps gl)
 
 let injEq flags ?(old=false) with_evars clear_flag ipats =
   (* Decide which compatibility mode to use *)
@@ -1716,8 +1716,8 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+  let hyps = Proofview.Goal.hyps gl in
+  let concl = Proofview.Goal.concl gl in
   (* The set of hypotheses using x *)
   let dephyps =
     List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) ->
@@ -1749,7 +1749,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
 
 let subst_one_var dep_proof_ok x =
   Proofview.Goal.enter begin fun gl ->
-    let gl = Proofview.Goal.assume gl in
     let decl = pf_get_hyp x gl in
     (* If x has a body, simply replace x with body and clear x *)
     if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else
@@ -1790,7 +1789,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
 
   (* First step: find hypotheses to treat in linear time *)
   let find_equations gl =
-    let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
     let sigma = project gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
@@ -1816,7 +1814,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () =
   (* Second step: treat equations *)
   let process hyp =
     Proofview.Goal.enter begin fun gl ->
-    let gl = Proofview.Goal.assume gl in
     let sigma = project gl in
     let env = Proofview.Goal.env gl in
     let find_eq_data_decompose = find_eq_data_decompose gl in
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 237ed42d5..01d916053 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -120,11 +120,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 : 'a Proofview.Goal.t -> constr ->
+val find_eq_data_decompose : Proofview.Goal.t -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
+val find_this_eq_data_decompose : Proofview.Goal.t -> constr ->
       coq_eq_data * EInstance.t * (types * constr * constr)
 
 (** A variant that returns more informative structure on the equality found *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index cb0bbfd0e..5435b63ce 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -353,7 +353,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     Proofview.Goal.enter begin fun gl ->
     let sigma = project gl in
     (** We only look at the type of hypothesis "id" *)
-    let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
+    let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in
     let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in
     match (EConstr.kind sigma t1, EConstr.kind sigma t2) with
     | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index cea6ccc30..e7da17cff 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -540,7 +540,6 @@ module New = struct
 
   let nthHypId m gl =
     (** We only use [id] *)
-    let gl = Proofview.Goal.assume gl in
     nthDecl m gl |> NamedDecl.get_id
   let nthHyp m gl = 
     mkVar (nthHypId m gl)
@@ -572,7 +571,7 @@ module New = struct
 
   let afterHyp id tac =
     Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let hyps = Proofview.Goal.hyps gl in
     let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in
     tac rem
     end
@@ -658,12 +657,12 @@ module New = struct
 
   let elimination_sort_of_goal gl =
     (** Retyping will expand evars anyway. *)
-    let c = Proofview.Goal.concl (Goal.assume gl) in
+    let c = Proofview.Goal.concl gl in
     pf_apply Retyping.get_sort_family_of gl c
 
   let elimination_sort_of_hyp id gl =
     (** Retyping will expand evars anyway. *)
-    let c = pf_get_hyp_typ id (Goal.assume gl) in
+    let c = pf_get_hyp_typ id gl in
     pf_apply Retyping.get_sort_family_of gl c
 
   let elimination_sort_of_clause id gl = match id with
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 55c519e24..c5d5c8c12 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -225,7 +225,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : 'a Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : Proofview.Goal.t -> int -> named_context
 
   val ifOnHyp     : (Id.t * types -> bool) ->
     (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) ->
@@ -236,7 +236,7 @@ module New : sig
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
   val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `LZ ] Proofview.Goal.t -> named_context) ->
+  val onHyps      : (Proofview.Goal.t -> named_context) ->
                     (named_context -> unit tactic) -> unit tactic
   val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
 
@@ -244,9 +244,9 @@ module New : sig
   val tryAllHypsAndConcl  : (Id.t option -> unit tactic) -> unit tactic
   val onClause   : (Id.t 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 : Proofview.Goal.t -> Sorts.family
+  val elimination_sort_of_hyp  : Id.t -> Proofview.Goal.t -> Sorts.family
+  val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family
 
   val elimination_then :
     (branch_args -> unit Proofview.tactic) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9fded04db..9011c4425 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -151,7 +151,6 @@ let unsafe_intro env store decl b =
 
 let introduction ?(check=true) id =
   Proofview.Goal.enter begin fun gl ->
-    let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let hyps = named_context_val (Proofview.Goal.env gl) in
@@ -258,7 +257,6 @@ let clear_gen fail = function
   Proofview.Goal.enter begin fun gl ->
     let ids = List.fold_right Id.Set.add ids Id.Set.empty in
     (** clear_hyps_in_evi does not require nf terms *)
-    let gl = Proofview.Goal.assume gl in
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
@@ -322,7 +320,6 @@ let rename_hyp repl =
   | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping")
   | Some (src, dst) ->
     Proofview.Goal.enter begin fun gl ->
-      let gl = Proofview.Goal.assume gl in
       let hyps = Proofview.Goal.hyps gl in
       let concl = Proofview.Goal.concl gl in
       let store = Proofview.Goal.extra gl in
@@ -814,7 +811,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm
 let e_change_in_hyp redfun (id,where) =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
+    let hyp = Tacmach.New.pf_get_hyp id gl in
     let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in
     Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
     (convert_hyp c)
@@ -981,7 +978,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Tacmach.New.pf_env gl in
-    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let concl = Proofview.Goal.concl gl in
     match EConstr.kind sigma concl with
     | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) ->
         let name = find_name false (LocalAssum (name,t)) name_flag gl in
@@ -1052,7 +1049,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
 let intro_replacing id =
   Proofview.Goal.enter begin fun gl ->
   let env, sigma = Proofview.Goal.(env gl, sigma gl) in
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+  let hyps = Proofview.Goal.hyps gl in
   let next_hyp = get_next_hyp_position env sigma id hyps in
   Tacticals.New.tclTHENLIST [
     clear_for_replacing [id];
@@ -1073,7 +1070,7 @@ let intros_possibly_replacing ids =
   let suboptimal = true in
   Proofview.Goal.enter begin fun gl ->
     let env, sigma = Proofview.Goal.(env gl, sigma gl) in
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let hyps = Proofview.Goal.hyps gl in
     let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
     Tacticals.New.tclTHEN
       (Tacticals.New.tclMAP (fun id -> 
@@ -1087,7 +1084,7 @@ let intros_possibly_replacing ids =
 (* This version assumes that replacement is actually possible *)
 let intros_replacing ids =
   Proofview.Goal.enter begin fun gl ->
-    let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
+    let hyps = Proofview.Goal.hyps gl in
     let env, sigma = Proofview.Goal.(env gl, sigma gl) in
     let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in
     Tacticals.New.tclTHEN
@@ -1150,7 +1147,7 @@ let intros_until_n = intros_until_n_gen true
 
 let tclCHECKVAR id =
   Proofview.Goal.enter begin fun gl ->
-    let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in
+    let _ = Tacmach.New.pf_get_hyp id gl in
     Proofview.tclUNIT ()
   end
 
@@ -1973,7 +1970,7 @@ let exact_check c =
   Proofview.Goal.enter begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
   (** We do not need to normalize the goal because we just check convertibility *)
-  let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+  let concl = Proofview.Goal.concl gl in
   let env = Proofview.Goal.env gl in
   let sigma, ct = Typing.type_of env sigma c in
   Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
@@ -1982,7 +1979,7 @@ let exact_check c =
 
 let cast_no_check cast c =
   Proofview.Goal.enter begin fun gl ->
-    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let concl = Proofview.Goal.concl gl in
     exact_no_check (mkCast (c, cast, concl))
   end
 
@@ -2066,7 +2063,7 @@ let clear_body ids =
   let open Context.Named.Declaration in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+    let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let ctx = named_context env in
     let map = function
@@ -2191,7 +2188,6 @@ let bring_hyps hyps =
 
 let revert hyps = 
   Proofview.Goal.enter begin fun gl ->
-    let gl = Proofview.Goal.assume gl in
     let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
       (bring_hyps ctx) <*> (clear hyps)
   end
@@ -2619,7 +2615,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars
     if with_evars then MoveLast (* evars would depend on the whole context *)
     else (
       let env, sigma = Proofview.Goal.(env gl, sigma gl) in
-      get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+      get_previous_hyp_position env sigma id (Proofview.Goal.hyps gl)
     ) in
   let naming,ipat_tac =
     prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in
@@ -2913,7 +2909,6 @@ end
 let new_generalize_gen_let lconstr =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
-    let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let ids = Tacmach.New.pf_ids_of_hyps gl in
@@ -3063,7 +3058,7 @@ let unfold_body x =
   let open Context.Named.Declaration in
   Proofview.Goal.enter begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
-  let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
+  let env = Proofview.Goal.env gl in
   let xval = match Environ.lookup_named x env with
   | LocalAssum _ -> user_err ~hdr:"unfold_body"
     (Id.print x ++ str" is not a defined hypothesis.")
@@ -3274,7 +3269,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Tacmach.New.project gl in
-  let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in
+  let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
   let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
   let typ0 = reduce_to_quantified_ref indref tmptyp0 in
   let prods, indtyp = decompose_prod_assum sigma typ0 in
@@ -4272,7 +4267,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
     let deps_cstr =
       List.fold_left
         (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in
-    let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in
+    let (sigma, isrec, elim, indsign) = get_eliminator elim dep s gl in
     let branchletsigns =
       let f (_,is_not_let,_,_) = is_not_let in
       Array.map (fun (_,l) -> List.map f l) indsign in
@@ -4297,7 +4292,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_
 
 let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps =
   Proofview.Goal.enter begin fun gl ->
-  let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in
+  let elim_info = find_induction_type isrec elim hyp0 gl in
   atomize_param_of_ind_then elim_info hyp0 (fun indvars ->
     apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names
       (fun elim -> induction_tac with_evars [] [hyp0] elim))
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 83fc655f1..483e790e5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -30,7 +30,7 @@ open Ltac_pretype
 
 (** {6 General functions. } *)
 
-val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool
+val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool
 
 (** {6 Primitive tactics. } *)
 
@@ -76,7 +76,7 @@ val intros               : unit Proofview.tactic
 (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in
    the conclusion of goal [g], up to head-reduction if [b] is [true] *)
 val depth_of_quantified_hypothesis :
-  bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int
+  bool -> quantified_hypothesis -> Proofview.Goal.t -> int
 
 val intros_until         : quantified_hypothesis -> unit Proofview.tactic