diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 15:28:29 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-06-13 15:28:29 +0000 |
| commit | f1bd83d9d6f69a0309572f1bfe22827d4c3f4eb7 (patch) | |
| tree | d36f10773968ed883c56e574c72f6c7e4f560e02 /contrib/first-order/sequent.mli | |
| parent | 89d58784a6e86f701bb8c619c32d62d546800d9f (diff) | |
Ground update, new files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4156 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/sequent.mli')
| -rw-r--r-- | contrib/first-order/sequent.mli | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/contrib/first-order/sequent.mli b/contrib/first-order/sequent.mli index 851396d45..79cf0d1ed 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/first-order/sequent.mli @@ -23,7 +23,9 @@ module OrderedConstr: Set.OrderedType with type t=constr module CM: Map.S with type key=constr -module History: Set.S with type elt = global_reference * constr option +type h_item = global_reference * (int*constr) option + +module History: Set.S with type elt = h_item val cm_add : constr -> global_reference -> global_reference list CM.t -> global_reference list CM.t @@ -43,9 +45,9 @@ type t = {redexes:HP.t; val deepen: t -> t -val record: global_reference -> constr option -> t -> t +val record: h_item -> t -> t -val lookup: global_reference -> constr option -> t -> bool +val lookup: h_item -> t -> bool val add_left : global_reference * constr -> t -> bool -> Proof_type.goal sigma -> t |