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. --- tactics/tacticals.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'tactics/tacticals.mli') 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) -> -- cgit v1.2.3