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

6 files changed, 17 insertions, 19 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index cfe69c705..23a21414d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -27,6 +27,7 @@ open Evarutil
 open Unification
 open Mod_subst
 open Coercion
+open Misctypes
 
 (* Abbreviations *)
 
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 04f532654..e0ad1acf9 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -17,6 +17,7 @@ open Evarutil
 open Mod_subst
 open Glob_term
 open Unification
+open Misctypes
 
 (** {6 The Type of Constructions clausale environments.} *)
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index bddf77d1f..21948b481 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -21,6 +21,7 @@ open Closure
 open RedFlags
 open Libobject
 open Summary
+open Misctypes
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env _ c =
@@ -169,8 +170,8 @@ let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
   | ArgArg x -> x
 
-let out_with_occurrences ((b,l),c) =
-  ((b,List.map out_arg l), c)
+let out_with_occurrences (occs,c) =
+  (Locusops.occurrences_map (List.map out_arg) occs, c)
 
 let rec reduction_of_red_expr = function
   | Red internal ->
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ae82153d2..99f942e11 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -13,6 +13,7 @@ open Pattern
 open Glob_term
 open Reductionops
 open Termops
+open Locus
 
 type red_expr =
     (constr, evaluable_global_reference, constr_pattern) red_expr_gen
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b48605657..4f960243c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -17,6 +17,8 @@ open Util
 open Genarg
 open Pattern
 open Decl_kinds
+open Misctypes
+open Locus
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
@@ -60,7 +62,7 @@ let make_red_flag =
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []}
 
-type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
 
 type 'id move_location =
   | MoveAfter of 'id
@@ -100,21 +102,12 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
-(* onhyps:
-     [None] means *on every hypothesis*
-     [Some l] means on hypothesis belonging to l *)
-type 'id gclause =
-  { onhyps : 'id raw_hyp_location list option;
-    concl_occs : occurrences_expr }
-
-let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
-
 type 'constr induction_clause =
   ('constr with_bindings induction_arg list * 'constr with_bindings option *
    (intro_pattern_expr located option * intro_pattern_expr located option))
 
 type ('constr,'id) induction_clause_list =
-    'constr induction_clause list * 'id gclause option
+    'constr induction_clause list * 'id clause_expr option
 
 type multi =
   | Precisely of int
@@ -162,7 +155,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
   | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of name * 'constr * 'id gclause * letin_flag
+  | TacLetTac of name * 'constr * 'id clause_expr * letin_flag
 
   (* Derived basic tactics *)
   | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
@@ -193,17 +186,17 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_atomic_tactic_expr =
   | TacConstructor of evars_flag * int or_var * 'constr bindings
 
   (* Conversion *)
-  | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id gclause
-  | TacChange of 'pat option * 'constr * 'id gclause
+  | TacReduce of ('constr,'cst,'pat) red_expr_gen * 'id clause_expr
+  | TacChange of 'pat option * 'constr * 'id clause_expr
 
   (* Equivalence relations *)
   | TacReflexivity
-  | TacSymmetry of 'id gclause
+  | TacSymmetry of 'id clause_expr
   | TacTransitivity of 'constr option
 
   (* Equality and inversion *)
   | TacRewrite of
-      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
+      evars_flag * (bool * multi * 'constr with_bindings) list * 'id clause_expr * 'tac option
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
 
   (* For ML extensions *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 402002de1..86a1edd76 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -18,6 +18,7 @@ open Redexpr
 open Tacexpr
 open Glob_term
 open Pattern
+open Locus
 
 (** Operations for handling terms under a local typing context. *)
 
@@ -71,7 +72,7 @@ val pf_nf_betaiota             : goal sigma -> constr -> constr
 val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
 val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
 val pf_compute                 : goal sigma -> constr -> constr
-val pf_unfoldn    : (Termops.occurrences * evaluable_global_reference) list
+val pf_unfoldn    : (occurrences * evaluable_global_reference) list
         -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> constant -> constr