diff options
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 8b72b3f210..6b955adac4 100644 --- a/contrib/first-order/sequent.mli +++ b/contrib/first-order/sequent.mli @@ -13,6 +13,7 @@ open Util open Formula open Tacmach open Names +open Libnames val right_reversible : right_pattern -> bool @@ -22,15 +23,15 @@ module CM: Map.S with type key=constr module HP: Heap.S with type elt=left_formula -type t = {hyps:HP.t;hatoms: identifier CM.t;gl:right_formula} +type t = {hyps:HP.t;hatoms: global_reference CM.t;gl:right_formula} -val add_left : identifier * constr -> t -> counter -> t +val add_left : global_reference * constr -> t -> bool -> counter -> t val re_add_left_list : left_formula list -> t -> t val change_right : constr -> t -> counter -> t -val find_left : constr -> t -> identifier +val find_left : constr -> t -> global_reference val rev_left : t -> bool @@ -42,3 +43,4 @@ val take_right : t -> right_formula val empty_seq : t +val create_with_auto_hints : Proof_type.goal sigma -> counter -> t |