X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2Fcontinuationals.mli;h=1dcf4aa7dc8fcc2a61af433ec7bb661a42520e32;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=293d056b34e30ef7b29413ee8aeb6990454fc711;hpb=0fde70bd19b8fdfa72b807b9713a02ad1bd91b5b;p=helm.git diff --git a/matita/components/ng_tactics/continuationals.mli b/matita/components/ng_tactics/continuationals.mli index 293d056b3..1dcf4aa7d 100644 --- a/matita/components/ng_tactics/continuationals.mli +++ b/matita/components/ng_tactics/continuationals.mli @@ -41,7 +41,6 @@ sig val find_goal: t -> goal (** find "next" goal *) val is_empty: t -> bool (** a singleton empty level *) - val of_metasenv: Cic.metasenv -> t val of_nmetasenv: (goal * 'a) list -> t val head_switches: t -> switch list (** top level switches *) val head_goals: t -> goal list (** top level goals *)