From 4ac1736bdbf55d3df4b56285958e57072d8b1534 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 20 Feb 2003 17:31:06 +0000 Subject: [PATCH] defined an explicit "status" type --- helm/ocaml/tactics/proofEngineTypes.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml index 974e6893c..178be54d4 100644 --- a/helm/ocaml/tactics/proofEngineTypes.ml +++ b/helm/ocaml/tactics/proofEngineTypes.ml @@ -29,12 +29,13 @@ type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term (** current goal, integer index *) type goal = int +type status = proof * goal (** a tactic: make a transition from one status to another one or, usually, raise a "Fail" (@see Fail) exception in case of failure *) (** an unfinished proof with the optional current goal *) -type tactic = status:(proof * goal) -> proof * goal list +type tactic = status:status -> proof * goal list (** tactic failure *) exception Fail of string -- 2.39.2