[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.

6 files changed, 31 insertions, 37 deletions

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