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

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`

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. *)
 

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

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
 

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)

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

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)

plugins/romega/const_omega.ml

@@ -223,15 +223,15 @@ 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
   val minus : constr Lazy.t
 
   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

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

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.")

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
 

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

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 =

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} *)

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

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

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

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