From 68935660fbfdec2e357e123ed999073ed3b8fc26 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Feb 2018 16:00:04 +0100
Subject: [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.
---
 engine/ftactic.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine/ftactic.mli')

diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index c108c0c2ea..65ee929c8c 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. *)
 
-- 
cgit v1.2.3