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

29 files changed, 168 insertions, 247 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 8b4f5eb611..6e338c4cbb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -42,6 +42,8 @@ open Printer
 open Declarations
 open Tacexpr
 open Mod_subst
+open Misctypes
+open Locus
 
 (****************************************************************************)
 (*            The Type of Constructions Autotactic Hints                    *)
@@ -1316,7 +1318,7 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t})) =
     | Unfold_nth c ->
       (fun gl ->
        if exists_evaluable_reference (pf_env gl) c then
-	 tclPROGRESS (h_reduce (Unfold [all_occurrences_expr,c]) onConcl) gl
+	 tclPROGRESS (h_reduce (Unfold [AllOccurrences,c]) Locusops.onConcl) gl
        else tclFAIL 0 (str"Unbound reference") gl)
     | Extern tacast -> conclPattern concl p tacast
   in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 49a7ef3055..0dfcb0b682 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -20,6 +20,7 @@ open Evd
 open Libnames
 open Vernacexpr
 open Mod_subst
+open Misctypes
 
 (** Auto and related automation tactics *)
 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 990da9306a..4981e70333 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -22,6 +22,7 @@ open Glob_term
 open Vernacinterp
 open Tacexpr
 open Mod_subst
+open Locus
 
 (* Rewriting rules *)
 type rew_rule = { rew_lemma: constr;
@@ -118,7 +119,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
        tclTHEN tac
         (one_base (fun dir c tac ->
 	  let tac = tac, conds in
-	    general_rewrite dir all_occurrences true false ~tac c)
+	    general_rewrite dir AllOccurrences true false ~tac c)
 	  tac_main bas))
       tclIDTAC lbas))
 
@@ -136,7 +137,7 @@ let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas : tactic =
       | _ -> (* even the hypothesis id is missing *)
              error ("No such hypothesis: " ^ (string_of_id !id) ^".")
     in
-    let gl' = general_rewrite_in dir all_occurrences true ~tac:(tac, conds) false !id cstr false gl in
+    let gl' = general_rewrite_in dir AllOccurrences true ~tac:(tac, conds) false !id cstr false gl in
     let gls = gl'.Evd.it in
     match gls with
        g::_ ->
@@ -172,8 +173,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
   let try_do_hyps treat_id l =
     autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas
   in
-  if cl.concl_occs <> all_occurrences_expr &
-     cl.concl_occs <> no_occurrences_expr
+  if cl.concl_occs <> AllOccurrences &
+     cl.concl_occs <> NoOccurrences
   then
     error "The \"at\" syntax isn't available yet for the autorewrite tactic."
   else
@@ -183,7 +184,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 	| _ ->      tclTHENFIRST t1 t2
     in
     compose_tac
-	(if cl.concl_occs <> no_occurrences_expr then autorewrite ~conds tac_main lbas else tclIDTAC)
+	(if cl.concl_occs <> NoOccurrences then autorewrite ~conds tac_main lbas else tclIDTAC)
 	(match cl.onhyps with
 	   | Some l -> try_do_hyps (fun ((_,id),_) -> id) l
 	   | None ->
@@ -196,8 +197,8 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
 let auto_multi_rewrite ?(conds=Naive) = gen_auto_multi_rewrite conds Refiner.tclIDTAC
 
 let auto_multi_rewrite_with ?(conds=Naive) tac_main lbas cl gl =
-  let onconcl = cl.Tacexpr.concl_occs <> no_occurrences_expr in
-  match onconcl,cl.Tacexpr.onhyps with
+  let onconcl = cl.Locus.concl_occs <> NoOccurrences in
+  match onconcl,cl.Locus.onhyps with
     | false,Some [_] | true,Some [] | false,Some [] ->
 	(* autorewrite with .... in clause using tac n'est sur que
 	   si clause represente soit le but soit UNE hypothese
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 6481217b6a..a3fc729595 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -35,9 +35,9 @@ val find_rewrites : string -> rew_rule list
 
 val find_matches : string -> constr -> rew_rule list
 
-val auto_multi_rewrite : ?conds:conditions -> string list -> Tacticals.clause -> tactic
+val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> tactic
 
-val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Tacticals.clause -> tactic
+val auto_multi_rewrite_with : ?conds:conditions -> tactic -> string list -> Locus.clause -> tactic
 
 val print_rewrite_hintdb : string -> unit
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f4c032e735..cafe17ad96 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -37,6 +37,8 @@ open Command
 open Libnames
 open Evd
 open Compat
+open Locus
+open Misctypes
 
 let typeclasses_db = "typeclass_instances"
 let typeclasses_debug = ref false
@@ -177,7 +179,7 @@ and e_my_find_search db_list local_db hdc complete concl =
 	  | Res_pf_THEN_trivial_fail (term,cl) ->
               tclTHEN (with_prods nprods (term,cl) (unify_e_resolve flags))
 	        (if complete then tclIDTAC else e_trivial_fail_db db_list local_db)
-	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [all_occurrences,c])
+	  | Unfold_nth c -> tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c])
 	  | Extern tacast -> 
 (* 	    tclTHEN *)
 (* 	      (fun gl -> Refiner.tclEVARS (mark_unresolvables (project gl)) gl) *)
@@ -807,7 +809,7 @@ let rec head_of_constr t =
 TACTIC EXTEND head_of_constr
   [ "head_of_constr" ident(h) constr(c) ] -> [
     let c = head_of_constr c in
-      letin_tac None (Name h) c None allHyps
+      letin_tac None (Name h) c None Locusops.allHyps
   ]
 END
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index c4cf7b62f4..76ee9ff680 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -17,6 +17,7 @@ open Tactics
 open Coqlib
 open Reductionops
 open Glob_term
+open Misctypes
 
 (* Absurd *)
 
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index b77b2721af..3020981392 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -9,8 +9,7 @@
 open Names
 open Term
 open Proof_type
-open Glob_term
-open Genarg
+open Misctypes
 
 val absurd                      : constr -> tactic
 val contradiction               : constr with_bindings option -> tactic
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 2700b2b7d5..8b773762f0 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -29,6 +29,9 @@ open Auto
 open Glob_term
 open Hiddentac
 open Tacexpr
+open Misctypes
+open Locus
+open Locusops
 
 let eauto_unif_flags = { auto_unif_flags with Unification.modulo_delta = full_transparent_state }
 
@@ -73,7 +76,7 @@ let prolog_tac l n gl =
   let l = List.map (prepare_hint (pf_env gl)) l in
   let n =
     match n with
-      |  ArgArg n -> n
+      | ArgArg n -> n
       | _ -> error "Prolog called with a non closed argument."
   in
   try (prolog l n gl)
@@ -134,7 +137,7 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Res_pf_THEN_trivial_fail (term,cl) ->
                tclTHEN (unify_e_resolve st (term,cl))
 		 (e_trivial_fail_db db_list local_db)
-	   | Unfold_nth c -> h_reduce (Unfold [all_occurrences_expr,c]) onConcl
+	   | Unfold_nth c -> h_reduce (Unfold [AllOccurrences,c]) onConcl
 	   | Extern tacast -> conclPattern concl p tacast
        in
        (tac,lazy (pr_autotactic t)))
@@ -459,12 +462,12 @@ let autounfolds db occs =
       with Not_found -> errorlabstrm "autounfold" (str "Unknown database " ++ str dbname)
     in
     let (ids, csts) = Hint_db.unfolds db in
-      Cset.fold (fun cst -> cons (all_occurrences, EvalConstRef cst)) csts
-	(Idset.fold (fun id -> cons (all_occurrences, EvalVarRef id)) ids [])) db)
+      Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts
+	(Idset.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db)
   in unfold_option unfolds
 
 let autounfold db cls gl =
-  let cls = concrete_clause_of cls gl in
+  let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
   let tac = autounfolds db in
   tclMAP (function
     | OnHyp (id,occs,where) -> tac occs (Some (id,where))
diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 5e656139be..e0893f439a 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -35,4 +35,4 @@ val eauto_with_bases :
   bool * int ->
   open_constr list -> Auto.hint_db list -> Proof_type.tactic
 
-val autounfold : hint_db_name list -> Tacticals.clause -> tactic
+val autounfold : hint_db_name list -> Locus.clause -> tactic
diff --git a/tactics/elim.mli b/tactics/elim.mli
index c40d1cbbc6..fe19c0b245 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -12,6 +12,7 @@ open Proof_type
 open Tacmach
 open Genarg
 open Tacticals
+open Misctypes
 
 (** Eliminations tactics. *)
 
@@ -30,5 +31,5 @@ val h_decompose       : inductive list -> constr -> tactic
 val h_decompose_or    : constr -> tactic
 val h_decompose_and   : constr -> tactic
 
-val double_ind : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis -> tactic
-val h_double_induction : Glob_term.quantified_hypothesis -> Glob_term.quantified_hypothesis->tactic
+val double_ind : quantified_hypothesis -> quantified_hypothesis -> tactic
+val h_double_induction : quantified_hypothesis -> quantified_hypothesis->tactic
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e3b62e496f..03f3811b77 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -45,6 +45,9 @@ open Clenvtac
 open Evd
 open Ind_tables
 open Eqschemes
+open Locus
+open Locusops
+open Misctypes
 
 (* Options *)
 
@@ -317,7 +320,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 
 let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars gl =
-  if occs <> all_occurrences then (
+  if occs <> AllOccurrences then (
     rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
   else
     let env = pf_env gl in
@@ -367,7 +370,7 @@ let general_rewrite_in l2r occs frzevars dep_proof_ok ?tac id c =
     frzevars dep_proof_ok ?tac (c,NoBindings)
 
 let general_multi_rewrite l2r with_evars ?tac c cl =
-  let occs_of = on_snd (List.fold_left
+  let occs_of = occurrences_map (List.fold_left
     (fun acc ->
       function ArgArg x -> x :: acc | ArgVar _ -> acc)
     [])
@@ -383,7 +386,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	      (general_rewrite_ebindings_in l2r (occs_of occs) false true ?tac id c with_evars)
 	      (do_hyps l)
 	in
-	if cl.concl_occs = no_occurrences_expr then do_hyps l else
+	if cl.concl_occs = NoOccurrences then do_hyps l else
 	  tclTHENFIRST
 	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   (do_hyps l)
@@ -394,7 +397,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	  | [] -> (fun gl -> error "Nothing to rewrite.")
 	  | id :: l ->
 	    tclIFTHENTRYELSEMUST
-	     (general_rewrite_ebindings_in l2r all_occurrences false true ?tac id c with_evars)
+	     (general_rewrite_ebindings_in l2r AllOccurrences false true ?tac id c with_evars)
 	     (do_hyps_atleastonce l)
 	in
 	let do_hyps gl =
@@ -404,7 +407,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl =
 	      Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl)
 	  in do_hyps_atleastonce ids gl
 	in
-	if cl.concl_occs = no_occurrences_expr then do_hyps else
+	if cl.concl_occs = NoOccurrences then do_hyps else
 	  tclIFTHENTRYELSEMUST
 	   (general_rewrite_ebindings l2r (occs_of cl.concl_occs) false true ?tac c with_evars)
 	   do_hyps
@@ -431,8 +434,8 @@ let general_multi_multi_rewrite with_evars l cl tac =
     | (l2r,m,c)::l -> tclTHENFIRST (doN l2r c m) (loop l)
   in loop l
 
-let rewriteLR = general_rewrite true all_occurrences true true
-let rewriteRL = general_rewrite false all_occurrences true true
+let rewriteLR = general_rewrite true AllOccurrences true true
+let rewriteRL = general_rewrite false AllOccurrences true true
 
 (* Replacing tactics *)
 
@@ -1439,7 +1442,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl =
   tclTHENLIST
     ((if need_rewrite then
       [generalize abshyps;
-       general_rewrite dir all_occurrences true dep_proof_ok (mkVar hyp);
+       general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
        thin dephyps;
        tclMAP introtac depdecls]
       else
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 12deb7d323..098e927219 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -25,6 +25,8 @@ open Termops
 open Glob_term
 open Genarg
 open Ind_tables
+open Locus
+open Misctypes
 (*i*)
 
 type dep_proof_flag = bool (* true = support rewriting dependent proofs *)
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a33b6b19bb..4b5229010f 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -16,7 +16,7 @@ open Refiner
 open Proof_type
 open Evd
 open Sign
-open Termops
+open Locus
 
 (* The instantiate tactic *)
 
@@ -55,4 +55,4 @@ let let_evar name typ gls =
   let src = (dummy_loc,Evar_kinds.GoalEvar) in
   let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) ~src typ in
   Refiner.tclTHEN (Refiner.tclEVARS sigma')
-    (Tactics.letin_tac None name evar None nowhere) gls
+    (Tactics.letin_tac None name evar None Locusops.nowhere) gls
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 882cf3ce68..f321604251 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -9,7 +9,7 @@
 open Tacmach
 open Names
 open Tacexpr
-open Termops
+open Locus
 
 val instantiate : int -> Tacinterp.interp_sign * Glob_term.glob_constr ->
   (identifier * hyp_location_flag, unit) location -> tactic
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index bd1145bd73..4677d87ef1 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -15,6 +15,8 @@ open Names
 open Tacexpr
 open Tacinterp
 open Termops
+open Misctypes
+open Locus
 
 (* Rewriting orientation *)
 
@@ -44,6 +46,14 @@ let pr_occurrences _prc _prlc _prt l =
     | ArgArg x -> pr_int_list x
     | ArgVar (loc, id) -> Nameops.pr_id id
 
+let occurrences_of = function
+  | [] -> NoOccurrences
+  | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl)
+  | nl ->
+      if List.exists (fun n -> n < 0) nl then
+        Errors.error "Illegal negative occurrence number.";
+      OnlyOccurrences nl
+
 let coerce_to_int = function
   | VInteger n -> n
   | v -> raise (CannotCoerceTo "an integer")
@@ -259,16 +269,16 @@ END
 
 let pr_in_arg_hyp = pr_in_arg_hyp_typed () () ()
 
-let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : Tacticals.clause =
-  {Tacexpr.onhyps=
+let gen_in_arg_hyp_to_clause trad_id (hyps ,concl) : clause =
+  {onhyps=
    Option.map
      (fun l ->
 	List.map
-	  (fun id -> ( (all_occurrences_expr,trad_id id),InHyp))
+	  (fun id -> ( (AllOccurrences,trad_id id),InHyp))
 	  l
      )
      hyps;
-   Tacexpr.concl_occs = if concl then all_occurrences_expr else no_occurrences_expr}
+   concl_occs = if concl then AllOccurrences else NoOccurrences}
 
 
 let raw_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause snd
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 35344c99c2..5d3691b548 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -13,6 +13,7 @@ open Proof_type
 open Topconstr
 open Termops
 open Glob_term
+open Misctypes
 
 val rawwit_orient : bool raw_abstract_argument_type
 val globwit_orient : bool glob_abstract_argument_type
@@ -23,13 +24,14 @@ val pr_orient : bool -> Pp.std_ppcmds
 val occurrences : (int list or_var) Pcoq.Gram.entry
 val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
-val pr_occurrences : int list Glob_term.or_var -> Pp.std_ppcmds
+val pr_occurrences : int list or_var -> Pp.std_ppcmds
+val occurrences_of : int list -> Locus.occurrences
 
 val rawwit_glob : constr_expr raw_abstract_argument_type
 val wit_glob : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type
 val glob : constr_expr Pcoq.Gram.entry
 
-type 'id gen_place= ('id * hyp_location_flag,unit) location
+type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 
 type loc_place = identifier Pp.located gen_place
 type place = identifier gen_place
@@ -43,8 +45,8 @@ val in_arg_hyp:  (Names.identifier Pp.located list option * bool)  Pcoq.Gram.ent
 val globwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) glob_abstract_argument_type
 val rawwit_in_arg_hyp : (Names.identifier Pp.located list option * bool) raw_abstract_argument_type
 val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
-val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Tacticals.clause
-val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Tacticals.clause
+val raw_in_arg_hyp_to_clause : (Names.identifier Pp.located list option * bool) -> Locus.clause
+val glob_in_arg_hyp_to_clause :  (Names.identifier list option * bool)  -> Locus.clause
 val pr_in_arg_hyp : (Names.identifier list option * bool) -> Pp.std_ppcmds
 
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e497581ed5..a2d1caf5f8 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -22,6 +22,7 @@ open Util
 open Evd
 open Equality
 open Compat
+open Misctypes
 
 (**********************************************************************)
 (* admit, replace, discriminate, injection, simplify_eq               *)
@@ -230,24 +231,17 @@ let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) =
   Refiner. tclWITHHOLES false
     (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings)) sigma true
 
-let occurrences_of = function
-  | n::_ as nl when n < 0 -> (false,List.map abs nl)
-  | nl ->
-      if List.exists (fun n -> n < 0) nl then
-	error "Illegal negative occurrence number.";
-      (true,nl)
-
 TACTIC EXTEND rewrite_star
 | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] ->
     [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] ->
     [ rewrite_star (Some id) o (occurrences_of occ) c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) "in" hyp(id) by_arg_tac(tac) ] ->
-    [ rewrite_star (Some id) o Termops.all_occurrences c tac ]
+    [ rewrite_star (Some id) o Locus.AllOccurrences c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) "at" occurrences(occ) by_arg_tac(tac) ] ->
     [ rewrite_star None o (occurrences_of occ) c tac ]
 | [ "rewrite" "*" orient(o) open_constr(c) by_arg_tac(tac) ] ->
-    [ rewrite_star None o Termops.all_occurrences c tac ]
+    [ rewrite_star None o Locus.AllOccurrences c tac ]
     END
 
 (**********************************************************************)
@@ -340,7 +334,7 @@ VERNAC COMMAND EXTEND DeriveInversionClear
   -> [ add_inversion_lemma_exn na c s false inv_clear_tac ]
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (Glob_term.GProp Term.Null) false inv_clear_tac ]
+  -> [ add_inversion_lemma_exn na c GProp false inv_clear_tac ]
 END
 
 open Term
@@ -351,7 +345,7 @@ VERNAC COMMAND EXTEND DeriveInversion
   -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (GProp Null) false inv_tac ]
+  -> [ add_inversion_lemma_exn na c GProp false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) hyp(id) ]
   -> [ inversion_lemma_from_goal 1 na id Term.prop_sort false inv_tac ]
@@ -660,7 +654,7 @@ exception Found of tactic
 
 let rewrite_except h g =
   tclMAP (fun id -> if id = h then tclIDTAC else 
-      tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true true id (mkVar h) false))
+      tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
     (Tacmach.pf_ids_of_hyps g) g
 
 
@@ -681,7 +675,7 @@ let  mkCaseEq a  : tactic =
          [Hiddentac.h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
           (fun g2 ->
 	    change_in_concl None
-	     (Tacred.pattern_occs [((false,[1]), a)] (Tacmach.pf_env g2) Evd.empty (Tacmach.pf_concl g2))
+	     (Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] (Tacmach.pf_env g2) Evd.empty (Tacmach.pf_concl g2))
 		  g2);
 	  simplest_case a] g);;
 
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 302bde6e68..8410e08ccd 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -16,6 +16,8 @@ open Genarg
 open Tacexpr
 open Tactics
 open Util
+open Locus
+open Misctypes
 
 (* Basic tactics *)
 let h_intro_move x y =
@@ -57,7 +59,7 @@ let h_generalize_gen cl =
   abstract_tactic (TacGeneralize cl)
     (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl))
 let h_generalize cl =
-  h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous))
+  h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous))
     cl)
 let h_generalize_dep c =
   abstract_tactic (TacGeneralizeDep c) (generalize_dep c)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index ca683cc24f..af7a2061b7 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -17,6 +17,7 @@ open Glob_term
 open Evd
 open Clenv
 open Termops
+open Misctypes
 
 (** Tactics for the interpreter. They left a trace in the proof tree
    when they are called. *)
@@ -53,12 +54,12 @@ val h_cofix           : identifier option -> tactic
 
 val h_cut             : constr -> tactic
 val h_generalize      : constr list -> tactic
-val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
+val h_generalize_gen  : (constr Locus.with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic
 val h_let_tac         : letin_flag -> name -> constr ->
-                        Tacticals.clause -> tactic
+                        Locus.clause -> tactic
 val h_let_pat_tac     : letin_flag -> name -> evar_map * constr ->
-                        Tacticals.clause -> tactic
+                        Locus.clause -> tactic
 
 (** Derived basic tactics *)
 
@@ -69,17 +70,17 @@ val h_new_induction   : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
-  Tacticals.clause option -> tactic
+  Locus.clause option -> tactic
 val h_new_destruct    : evars_flag ->
   (evar_map * constr with_bindings) induction_arg list ->
   constr with_bindings option ->
   intro_pattern_expr located option * intro_pattern_expr located option ->
-  Tacticals.clause option -> tactic
+  Locus.clause option -> tactic
 val h_induction_destruct : rec_flag -> evars_flag ->
   ((evar_map * constr with_bindings) induction_arg list *
    constr with_bindings option *
    (intro_pattern_expr located option * intro_pattern_expr located option)) list
-    * Tacticals.clause option -> tactic
+    * Locus.clause option -> tactic
 
 val h_specialize      : int option -> constr with_bindings -> tactic
 val h_lapply          : constr -> tactic
@@ -106,13 +107,13 @@ val h_simplest_right  : tactic
 
 
 (** Conversion *)
-val h_reduce          : Redexpr.red_expr -> Tacticals.clause -> tactic
+val h_reduce          : Redexpr.red_expr -> Locus.clause -> tactic
 val h_change          :
-  Pattern.constr_pattern option -> constr -> Tacticals.clause -> tactic
+  Pattern.constr_pattern option -> constr -> Locus.clause -> tactic
 
 (** Equivalence relations *)
 val h_reflexivity     : tactic
-val h_symmetry        : Tacticals.clause -> tactic
+val h_symmetry        : Locus.clause -> tactic
 val h_transitivity    : constr option -> tactic
 
 val h_simplest_apply  : constr -> tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 47e50d8327..f5762768ef 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -34,7 +34,7 @@ open Typing
 open Pattern
 open Matching
 open Glob_term
-open Genarg
+open Misctypes
 open Tacexpr
 
 let collect_meta_variables c =
diff --git a/tactics/inv.mli b/tactics/inv.mli
index a7e70dd0d5..7dc9feb2c7 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -10,7 +10,7 @@ open Pp
 open Names
 open Term
 open Tacmach
-open Genarg
+open Misctypes
 open Tacexpr
 open Glob_term
 
diff --git a/tactics/leminv.mli b/tactics/leminv.mli
index d5deff1f53..21fcc0f5d2 100644
--- a/tactics/leminv.mli
+++ b/tactics/leminv.mli
@@ -4,6 +4,7 @@ open Term
 open Glob_term
 open Proof_type
 open Topconstr
+open Misctypes
 
 val lemInv_gen : quantified_hypothesis -> constr -> tactic
 val lemInvIn_gen : quantified_hypothesis -> constr -> identifier list -> tactic
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 88170d6dd7..04a1734fb4 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -38,6 +38,10 @@ open Command
 open Libnames
 open Evd
 open Compat
+open Misctypes
+open Locus
+open Locusops
+open Decl_kinds
 
 (** Typeclass-based generalized rewriting. *)
 
@@ -631,7 +635,7 @@ let apply_constraint env avoid car rel prf cstr res =
 let eq_env x y = x == y
 
 let apply_rule hypinfo loccs : strategy =
-  let (nowhere_except_in,occs) = loccs in
+  let (nowhere_except_in,occs) = convert_occs loccs in
   let is_occ occ =
     if nowhere_except_in then List.mem occ occs else not (List.mem occ occs) in
   let occ = ref 0 in
@@ -1007,7 +1011,7 @@ module Strategies =
 
     let lemmas flags cs : strategy =
       List.fold_left (fun tac (l,l2r) ->
-	choice tac (apply_lemma flags l l2r (false,[])))
+	choice tac (apply_lemma flags l l2r AllOccurrences))
 	fail cs
 
     let inj_open c = (Evd.empty,c)
@@ -1386,8 +1390,8 @@ ARGUMENT EXTEND rewstrategy TYPED AS strategy
     GLOBALIZED BY glob_strategy
     SUBSTITUTED BY subst_strategy
 
-    [ constr(c) ] -> [ apply_constr_expr c true all_occurrences ]
-  | [ "<-" constr(c) ] -> [ apply_constr_expr c false all_occurrences ]
+    [ constr(c) ] -> [ apply_constr_expr c true AllOccurrences ]
+  | [ "<-" constr(c) ] -> [ apply_constr_expr c false AllOccurrences ]
   | [ "subterms" rewstrategy(h) ] -> [ all_subterms h ]
   | [ "subterm" rewstrategy(h) ] -> [ one_subterm h ]
   | [ "innermost" rewstrategy(h) ] -> [ Strategies.innermost h ]
@@ -1425,7 +1429,7 @@ let clsubstitute o c =
       (fun cl ->
 	match cl with
 	  | Some id when is_tac id -> tclIDTAC
-	  | _ -> cl_rewrite_clause c o all_occurrences cl)
+	  | _ -> cl_rewrite_clause c o AllOccurrences cl)
 
 open Extraargs
 
@@ -1438,9 +1442,9 @@ END
 
 TACTIC EXTEND setoid_rewrite
    [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-   -> [ cl_rewrite_clause c o all_occurrences None ]
+   -> [ cl_rewrite_clause c o AllOccurrences None ]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-      [ cl_rewrite_clause c o all_occurrences (Some id)]
+      [ cl_rewrite_clause c o AllOccurrences (Some id)]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
       [ cl_rewrite_clause c o (occurrences_of occ) None]
  | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
@@ -1459,11 +1463,11 @@ TACTIC EXTEND GenRew
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] ->
     [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
-    [ cl_rewrite_clause_newtac_tac c o all_occurrences (Some id) ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
     [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ]
 | [ "rew" orient(o) glob_constr_with_bindings(c) ] ->
-    [ cl_rewrite_clause_newtac_tac c o all_occurrences None ]
+    [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ]
 END
 
 let mkappc s l = CAppExpl (dummy_loc,(None,(Libnames.Ident (dummy_loc,id_of_string s))),l)
@@ -1899,7 +1903,7 @@ let setoid_transitivity c gl =
       let proof = get_transitive_proof env evm car rel in
       match c with
       | None -> eapply proof
-      | Some c -> apply_with_bindings (proof,Glob_term.ImplicitBindings [ c ]))
+      | Some c -> apply_with_bindings (proof,ImplicitBindings [ c ]))
     (transitivity_red true c)
 
 let setoid_symmetry_in id gl =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1dc0f6589b..0d277855f7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -48,6 +48,8 @@ open Extrawit
 open Pcoq
 open Compat
 open Evd
+open Misctypes
+open Locus
 
 let safe_msgnl s =
     try msgnl s with e ->
@@ -164,7 +166,7 @@ let add_primitive_tactic s tac =
   atomic_mactab := Idmap.add id tac !atomic_mactab
 
 let _ =
-  let nocl = {onhyps=Some[];concl_occs=all_occurrences_expr} in
+  let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
   List.iter
       (fun (s,t) -> add_primitive_tactic s (TacAtom(dloc,t)))
       [ "red", TacReduce(Red false,nocl);
@@ -588,8 +590,9 @@ let intern_inversion_strength lf ist = function
       InversionUsing (intern_constr ist c, intern_hyp_list ist idl)
 
 (* Interprets an hypothesis name *)
-let intern_hyp_location ist (((b,occs),id),hl) =
-  (((b,List.map (intern_or_var ist) occs),intern_hyp_or_metaid ist id), hl)
+let intern_hyp_location ist ((occs,id),hl) =
+  ((Locusops.occurrences_map (List.map (intern_or_var ist)) occs,
+   intern_hyp_or_metaid ist id), hl)
 
 (* Reads a pattern *)
 let intern_pattern ist ?(as_type=false) lfun = function
@@ -764,8 +767,8 @@ let rec intern_atomic lf ist x =
   | TacChange (None,c,cl) ->
       TacChange (None,
         (if (cl.onhyps = None or cl.onhyps = Some []) &
-	    (cl.concl_occs = all_occurrences_expr or
-	     cl.concl_occs = no_occurrences_expr)
+	    (cl.concl_occs = AllOccurrences or
+	     cl.concl_occs = NoOccurrences)
          then intern_type ist c else intern_constr ist c),
 	clause_app (intern_hyp_location ist) cl)
   | TacChange (Some p,c,cl) ->
@@ -1179,8 +1182,8 @@ let interp_evaluable ist env = function
       interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
 
 (* Interprets an hypothesis name *)
-let interp_occurrences ist (b,occs) =
-  (b,interp_int_or_var_list ist occs)
+let interp_occurrences ist occs =
+  Locusops.occurrences_map (interp_int_or_var_list ist) occs
 
 let interp_hyp_location ist gl ((occs,id),hl) =
   ((interp_occurrences ist occs,interp_hyp ist gl id),hl)
@@ -1347,8 +1350,8 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma occl =
 
 let interp_constr_with_occurrences_and_name_as_list =
   interp_constr_in_compound_list
-    (fun c -> ((all_occurrences_expr,c),Anonymous))
-    (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c
+    (fun c -> ((AllOccurrences,c),Anonymous))
+    (function ((occs,c),Anonymous) when occs = AllOccurrences -> c
       | _ -> raise Not_found)
     (fun ist env sigma (occ_c,na) ->
       let (sigma,c_interp) = interp_constr_with_occurrences ist env sigma occ_c in
@@ -2390,7 +2393,7 @@ and interp_atomic ist gl tac =
 	(h_generalize_dep c_interp)
   | TacLetTac (na,c,clp,b) ->
       let clp = interp_clause ist gl clp in
-      if clp = nowhere then
+      if clp = Locusops.nowhere then
         (* We try to fully-typechect the term *)
 	let (sigma,c_interp) = pf_interp_constr ist gl c in
 	tclTHEN
@@ -2491,8 +2494,8 @@ and interp_atomic ist gl tac =
   | TacChange (None,c,cl) ->
       let (sigma,c_interp) =
 	if (cl.onhyps = None or cl.onhyps = Some []) &
-	    (cl.concl_occs = all_occurrences_expr or
-	     cl.concl_occs = no_occurrences_expr)
+	    (cl.concl_occs = AllOccurrences or
+	     cl.concl_occs = NoOccurrences)
 	 then pf_interp_type ist gl c
 	 else pf_interp_constr ist gl c
       in
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 991fbc88c7..861dcb97c4 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -19,6 +19,7 @@ open Genarg
 open Topconstr
 open Mod_subst
 open Redexpr
+open Misctypes
 
 (** Values for interpretation *)
 type value =
@@ -101,8 +102,8 @@ val intern_constr :
   glob_sign -> constr_expr -> glob_constr_and_expr
 
 val intern_constr_with_bindings :
-  glob_sign -> constr_expr * constr_expr Glob_term.bindings ->
-  glob_constr_and_expr * glob_constr_and_expr Glob_term.bindings
+  glob_sign -> constr_expr * constr_expr bindings ->
+  glob_constr_and_expr * glob_constr_and_expr bindings
 
 val intern_hyp :
   glob_sign -> identifier Pp.located -> identifier Pp.located
@@ -114,7 +115,7 @@ val subst_glob_constr_and_expr :
   substitution -> glob_constr_and_expr -> glob_constr_and_expr
 
 val subst_glob_with_bindings :
-  substitution -> glob_constr_and_expr Glob_term.with_bindings -> glob_constr_and_expr Glob_term.with_bindings
+  substitution -> glob_constr_and_expr with_bindings -> glob_constr_and_expr with_bindings
 
 (** Interprets any expression *)
 val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value
@@ -132,10 +133,11 @@ val interp_tac_gen : (identifier * value) list -> identifier list ->
 
 val interp_hyp :  interp_sign -> goal sigma -> identifier located -> identifier
 
-val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr Glob_term.bindings -> Evd.evar_map * constr Glob_term.bindings
+val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
+ glob_constr_and_expr bindings -> Evd.evar_map * constr bindings
 
-val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map -> 
-  glob_constr_and_expr Glob_term.with_bindings -> Evd.evar_map * constr Glob_term.with_bindings
+val interp_open_constr_with_bindings : interp_sign -> Environ.env -> Evd.evar_map ->
+  glob_constr_and_expr with_bindings -> Evd.evar_map * constr with_bindings
 
 (** Initial call for interpretation *)
 val glob_tactic : raw_tactic_expr -> glob_tactic_expr
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f7b8419c97..c95486df61 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -27,6 +27,8 @@ open Pattern
 open Matching
 open Genarg
 open Tacexpr
+open Locus
+open Misctypes
 
 (************************************************************************)
 (* Tacticals re-exported from the Refiner module                        *)
@@ -131,43 +133,6 @@ let afterHyp id gl =
    --Eduardo (8/8/97)
 *)
 
-(* A [simple_clause] is a set of hypotheses, possibly extended with
-   the conclusion (conclusion is represented by None) *)
-
-type simple_clause = identifier option list
-
-(* An [clause] is the algebraic form of a
-   [concrete_clause]; it may refer to all hypotheses
-   independently of the effective contents of the current goal *)
-
-type clause = identifier gclause
-
-let allHypsAndConcl = { onhyps=None; concl_occs=all_occurrences_expr }
-let allHyps = { onhyps=None; concl_occs=no_occurrences_expr }
-let onConcl = { onhyps=Some[]; concl_occs=all_occurrences_expr }
-let onHyp id =
-  { onhyps=Some[((all_occurrences_expr,id),InHyp)];
-    concl_occs=no_occurrences_expr }
-
-let simple_clause_of cl gls =
-  let error_occurrences () =
-    error "This tactic does not support occurrences selection" in
-  let error_body_selection () =
-    error "This tactic does not support body selection" in
-  let hyps =
-    match cl.onhyps with
-    | None ->
-	List.map Option.make (pf_ids_of_hyps gls)
-    | Some l ->
-	List.map (fun ((occs,id),w) ->
-	  if occs <> all_occurrences_expr then error_occurrences ();
-	  if w = InHypValueOnly then error_body_selection ();
-	  Some id) l in
-  if cl.concl_occs = no_occurrences_expr then hyps
-  else
-    if cl.concl_occs <> all_occurrences_expr then error_occurrences ()
-    else None :: hyps
-
 let fullGoal gl = None :: List.map Option.make (pf_ids_of_hyps gl)
 
 let onAllHyps tac gl = tclMAP tac (pf_ids_of_hyps gl) gl
@@ -176,8 +141,12 @@ let onAllHypsAndConcl tac gl = tclMAP tac (fullGoal gl) gl
 let tryAllHyps tac gl = tclFIRST_PROGRESS_ON tac (pf_ids_of_hyps gl) gl
 let tryAllHypsAndConcl tac gl = tclFIRST_PROGRESS_ON tac (fullGoal gl) gl
 
-let onClause tac cl gls = tclMAP tac (simple_clause_of cl gls) gls
-let onClauseLR tac cl gls = tclMAP tac (List.rev (simple_clause_of cl gls)) gls
+let onClause tac cl gls =
+  let hyps () = pf_ids_of_hyps gls in
+  tclMAP tac (Locusops.simple_clause_of hyps cl) gls
+let onClauseLR tac cl gls =
+  let hyps () = pf_ids_of_hyps gls in
+  tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls
 
 let ifOnHyp pred tac1 tac2 id gl =
   if pred (id,pf_get_hyp_typ gl id) then
@@ -185,52 +154,6 @@ let ifOnHyp pred tac1 tac2 id gl =
   else
     tac2 id gl
 
-
-(************************************************************************)
-(* An intermediate form of occurrence clause that select components     *)
-(* of a definition, hypotheses and possibly the goal                    *)
-(* (used for reduction tactics)                                         *)
-(************************************************************************)
-
-(* A [hyp_location] is an hypothesis together with a position, in
-   body if any, in type or in both *)
-
-type hyp_location = identifier * hyp_location_flag
-
-(* A [goal_location] is either an hypothesis (together with a position, in
-   body if any, in type or in both) or the goal *)
-
-type goal_location = hyp_location option
-
-(************************************************************************)
-(* An intermediate structure for dealing with occurrence clauses        *)
-(************************************************************************)
-
-(* [clause_atom] refers either to an hypothesis location (i.e. an
-   hypothesis with occurrences and a position, in body if any, in type
-   or in both) or to some occurrences of the conclusion *)
-
-type clause_atom =
-  | OnHyp of identifier * occurrences_expr * hyp_location_flag
-  | OnConcl of occurrences_expr
-
-(* A [concrete_clause] is an effective collection of
-  occurrences in the hypotheses and the conclusion *)
-
-type concrete_clause = clause_atom list
-
-let concrete_clause_of cl gls =
-  let hyps =
-    match cl.onhyps with
-    | None ->
-	let f id = OnHyp (id,all_occurrences_expr,InHyp) in
-	List.map f (pf_ids_of_hyps gls)
-    | Some l ->
-	List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in
-  if cl.concl_occs = no_occurrences_expr then hyps
-  else
-    OnConcl cl.concl_occs :: hyps
-
 (************************************************************************)
 (* Elimination Tacticals                                                *)
 (************************************************************************)
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 7c13894ec9..d4cbc6e5b2 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -21,6 +21,8 @@ open Genarg
 open Tacexpr
 open Termops
 open Glob_term
+open Locus
+open Misctypes
 
 (** Tacticals i.e. functions from tactics to tactics. *)
 
@@ -94,24 +96,10 @@ val onHyps      : (goal sigma -> named_context) ->
 
 (** {6 Tacticals applying to goal components } *)
 
-(** A [simple_clause] is a set of hypotheses, possibly extended with
-   the conclusion (conclusion is represented by None) *)
-
-type simple_clause = identifier option list
-
 (** A [clause] denotes occurrences and hypotheses in a
    goal; in particular, it can abstractly refer to the set of
    hypotheses independently of the effective contents of the current goal *)
 
-type clause = identifier gclause
-
-val simple_clause_of : clause -> goal sigma -> simple_clause
-
-val allHypsAndConcl : clause
-val allHyps         : clause
-val onHyp           : identifier -> clause
-val onConcl         : clause
-
 val tryAllHyps          : (identifier -> tactic) -> tactic
 val tryAllHypsAndConcl  : (identifier option -> tactic) -> tactic
 
@@ -121,36 +109,6 @@ val onAllHypsAndConcl   : (identifier option -> tactic) -> tactic
 val onClause   : (identifier option -> tactic) -> clause -> tactic
 val onClauseLR : (identifier option -> tactic) -> clause -> tactic
 
-(** {6 An intermediate form of occurrence clause with no mention of occurrences } *)
-
-(** A [hyp_location] is an hypothesis together with a position, in
-   body if any, in type or in both *)
-
-type hyp_location = identifier * hyp_location_flag
-
-(** A [goal_location] is either an hypothesis (together with a position, in
-   body if any, in type or in both) or the goal *)
-
-type goal_location = hyp_location option
-
-(** {6 A concrete view of occurrence clauses } *)
-
-(** [clause_atom] refers either to an hypothesis location (i.e. an
-   hypothesis with occurrences and a position, in body if any, in type
-   or in both) or to some occurrences of the conclusion *)
-
-type clause_atom =
-  | OnHyp of identifier * occurrences_expr * hyp_location_flag
-  | OnConcl of occurrences_expr
-
-(** A [concrete_clause] is an effective collection of
-  occurrences in the hypotheses and the conclusion *)
-
-type concrete_clause = clause_atom list
-
-(** This interprets an [clause] in a given [goal] context *)
-val concrete_clause_of : clause -> goal sigma -> concrete_clause
-
 (** {6 Elimination tacticals. } *)
 
 type branch_args = {
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4ac2a5bc7..7e350bfe90 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -44,6 +44,9 @@ open Evarutil
 open Indrec
 open Pretype_errors
 open Unification
+open Locus
+open Locusops
+open Misctypes
 
 exception Bound
 
@@ -56,7 +59,7 @@ let rec nb_prod x =
       | _ -> n
   in count 0 x
 
-let inj_with_occurrences e = (all_occurrences_expr,e)
+let inj_with_occurrences e = (AllOccurrences,e)
 
 let dloc = dummy_loc
 
@@ -228,11 +231,11 @@ let bind_change_occurrences occs = function
 
 let bind_red_expr_occurrences occs nbcl redexp =
   let has_at_clause = function
-    | Unfold l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l
-    | Pattern l -> List.exists (fun (occl,_) -> occl <> all_occurrences_expr) l
-    | Simpl (Some (occl,_)) -> occl <> all_occurrences_expr
+    | Unfold l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l
+    | Pattern l -> List.exists (fun (occl,_) -> occl <> AllOccurrences) l
+    | Simpl (Some (occl,_)) -> occl <> AllOccurrences
     | _ -> false in
-  if occs = all_occurrences_expr then
+  if occs = AllOccurrences then
     if nbcl > 1 && has_at_clause redexp then
       error_illegal_non_atomic_clause ()
     else
@@ -242,24 +245,24 @@ let bind_red_expr_occurrences occs nbcl redexp =
     | Unfold (_::_::_) ->
 	error_illegal_clause ()
     | Unfold [(occl,c)] ->
-	if occl <> all_occurrences_expr then
+	if occl <> AllOccurrences then
 	  error_illegal_clause ()
 	else
 	  Unfold [(occs,c)]
     | Pattern (_::_::_) ->
 	error_illegal_clause ()
     | Pattern [(occl,c)] ->
-	if occl <> all_occurrences_expr then
+	if occl <> AllOccurrences then
 	  error_illegal_clause ()
 	else
 	  Pattern [(occs,c)]
     | Simpl (Some (occl,c)) ->
-	if occl <> all_occurrences_expr then
+	if occl <> AllOccurrences then
 	  error_illegal_clause ()
 	else
 	  Simpl (Some (occs,c))
     | CbvVm (Some (occl,c)) ->
-        if occl <> all_occurrences_expr then
+        if occl <> AllOccurrences then
           error_illegal_clause ()
         else
           CbvVm (Some (occs,c))
@@ -312,7 +315,7 @@ let change_option occl t = function
   | None -> change_in_concl occl t
 
 let change chg c cls gl =
-  let cls = concrete_clause_of cls gl in
+  let cls = concrete_clause_of (fun () -> pf_ids_of_hyps gl) cls in
   tclMAP (function
     | OnHyp (id,occs,where) ->
        change_option (bind_change_occurrences occs chg) c (Some (id,where))
@@ -351,7 +354,7 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl goal =
-  let cl = concrete_clause_of cl goal in
+  let cl = concrete_clause_of (fun () -> pf_ids_of_hyps goal) cl in
   let redexps = reduction_clause redexp cl in
   let tac = tclMAP (fun (where,redexp) ->
     reduct_option (Redexpr.reduction_of_red_expr redexp) where) redexps in
@@ -362,8 +365,8 @@ let reduce redexp cl goal =
 (* Unfolding occurrences of a constant *)
 
 let unfold_constr = function
-  | ConstRef sp -> unfold_in_concl [all_occurrences,EvalConstRef sp]
-  | VarRef id -> unfold_in_concl [all_occurrences,EvalVarRef id]
+  | ConstRef sp -> unfold_in_concl [AllOccurrences,EvalConstRef sp]
+  | VarRef id -> unfold_in_concl [AllOccurrences,EvalVarRef id]
   | _ -> errorlabstrm "unfold_constr" (str "Cannot unfold a non-constant.")
 
 (*******************************************)
@@ -1548,7 +1551,7 @@ let generalize_dep ?(with_let=false) c gl =
       | _ -> None
     else None
   in
-  let cl'' = generalize_goal gl 0 ((all_occurrences,c,body),Anonymous) cl' in
+  let cl'' = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous) cl' in
   let args = Array.to_list (instance_from_named_context to_quantify_rev) in
   tclTHEN
     (apply_type cl'' (if body = None then c::args else args))
@@ -1566,7 +1569,7 @@ let generalize_gen lconstr =
     (occs,c,None),na) lconstr)
     
 let generalize l =
-  generalize_gen_let (List.map (fun c -> ((all_occurrences,c,None),Anonymous)) l)
+  generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l)
 
 let pf_get_hyp_val gl id =
   let (_, b, _) = pf_get_hyp gl id in
@@ -1574,7 +1577,7 @@ let pf_get_hyp_val gl id =
 
 let revert hyps gl = 
   let lconstr = List.map (fun id -> 
-    ((all_occurrences, mkVar id, pf_get_hyp_val gl id), Anonymous)) 
+    ((AllOccurrences, mkVar id, pf_get_hyp_val gl id), Anonymous))
     hyps 
   in tclTHEN (generalize_gen_let lconstr) (clear hyps) gl
 
@@ -1621,15 +1624,16 @@ let out_arg = function
 let occurrences_of_hyp id cls =
   let rec hyp_occ = function
       [] -> None
-    | (((b,occs),id'),hl)::_ when id=id' -> Some ((b,List.map out_arg occs),hl)
+    | ((occs,id'),hl)::_ when id=id' ->
+        Some (occurrences_map (List.map out_arg) occs, hl)
     | _::l -> hyp_occ l in
   match cls.onhyps with
-      None -> Some (all_occurrences,InHyp)
+      None -> Some (AllOccurrences,InHyp)
     | Some l -> hyp_occ l
 
 let occurrences_of_goal cls =
-  if cls.concl_occs = no_occurrences_expr then None
-  else Some (on_snd (List.map out_arg) cls.concl_occs)
+  if cls.concl_occs = NoOccurrences then None
+  else Some (occurrences_map (List.map out_arg) cls.concl_occs)
 
 let in_every_hyp cls = (cls.onhyps=None)
 
@@ -1732,7 +1736,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl =
       | None -> depdecls
       | Some occ ->
           let newdecl = subst_closed_term_occ_decl_modulo occ test d in
-          if occ = (all_occurrences,InHyp) & eq_named_declaration d newdecl then
+          if occ = (AllOccurrences,InHyp) & eq_named_declaration d newdecl then
 	    if check_occs & not (in_every_hyp occs)
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
@@ -3056,9 +3060,9 @@ let induction_without_atomization isrec with_evars elim names lid gl =
 let has_selected_occurrences = function
   | None -> false
   | Some cls ->
-      cls.concl_occs <> all_occurrences_expr ||
+      cls.concl_occs <> AllOccurrences ||
 	cls.onhyps <> None && List.exists (fun ((occs,_),hl) ->
-          occs <> all_occurrences_expr || hl <> InHyp) (Option.get cls.onhyps)
+          occs <> AllOccurrences || hl <> InHyp) (Option.get cls.onhyps)
 
 (* assume that no occurrences are selected *)
 let clear_unselected_context id inhyps cls gl =
@@ -3066,7 +3070,7 @@ let clear_unselected_context id inhyps cls gl =
   | None -> tclIDTAC gl
   | Some cls ->
       if occur_var (pf_env gl) id (pf_concl gl) &&
-	 cls.concl_occs = no_occurrences_expr
+	 cls.concl_occs = NoOccurrences
       then errorlabstrm ""
 	    (str "Conclusion must be mentioned: it depends on " ++ pr_id id
 	     ++ str ".");
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6e3c2cff46..40bcb94c92 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -28,6 +28,8 @@ open Glob_term
 open Pattern
 open Termops
 open Unification
+open Misctypes
+open Locus
 
 (** Main tactics. *)