locus.mli for occurrences+clauses, misctypes.mli for various little things

 Corresponding operations in locusops.ml and miscops.ml

 The type of occurrences is now a clear algebraic one instead of
 a bool*list hard to understand.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 34 insertions, 0 deletions

diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
new file mode 100644
index 000000000..285d9412e
--- /dev/null
+++ b/pretyping/locusops.mli
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Misctypes
+open Locus
+
+(** Utilities on occurrences *)
+
+val occurrences_map :
+  ('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen
+
+(** From occurrences to a list of positions (or complement of positions) *)
+val convert_occs : occurrences -> bool * int list
+
+val is_selected : int -> occurrences -> bool
+
+(** Usual clauses *)
+
+val allHypsAndConcl : 'a clause_expr
+val allHyps : 'a clause_expr
+val onConcl : 'a clause_expr
+val nowhere : 'a clause_expr
+val onHyp : 'a -> 'a clause_expr
+
+(** Clause conversion functions, parametrized by a hyp enumeration function *)
+
+val simple_clause_of : (unit -> identifier list) -> clause -> simple_clause
+val concrete_clause_of : (unit -> identifier list) -> clause -> concrete_clause