From 7d220f8b61649646692983872626d6a8042446a9 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 20 Mar 2009 01:22:58 +0000
Subject: Directory 'contrib' renamed into 'plugins', to end confusion with
 archive of user contribs

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/firstorder/sequent.mli | 66 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 plugins/firstorder/sequent.mli

(limited to 'plugins/firstorder/sequent.mli')

diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
new file mode 100644
index 000000000..51db9de16
--- /dev/null
+++ b/plugins/firstorder/sequent.mli
@@ -0,0 +1,66 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id$ *)
+
+open Term
+open Util
+open Formula
+open Tacmach
+open Names
+open Libnames
+
+module OrderedConstr: Set.OrderedType with type t=constr
+
+module CM: Map.S with type key=constr
+
+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
+
+val cm_remove : constr -> global_reference -> global_reference list CM.t ->
+  global_reference list CM.t
+
+module HP: Heap.S with type elt=Formula.t
+
+type t = {redexes:HP.t;
+	  context: global_reference list CM.t;
+	  latoms:constr list;
+	  gl:types;
+	  glatom:constr option;
+	  cnt:counter;
+	  history:History.t;
+	  depth:int}
+
+val deepen: t -> t
+
+val record: h_item -> t -> t
+
+val lookup: h_item -> t -> bool
+
+val add_formula : side -> global_reference -> constr -> t -> 
+  Proof_type.goal sigma -> t
+
+val re_add_formula_list : Formula.t list -> t -> t
+
+val find_left : constr -> t -> global_reference
+
+val take_formula : t -> Formula.t * t
+
+val empty_seq : int -> t
+
+val create_with_ref_list : global_reference list ->
+  int -> Proof_type.goal sigma -> t
+
+val create_with_auto_hints : Auto.hint_db_name list -> 
+  int -> Proof_type.goal sigma -> t
+
+val print_cmap: global_reference list CM.t -> unit 
-- 
cgit v1.2.3