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

21 files changed, 257 insertions, 133 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33e1ecdf2..832d32086 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -25,6 +25,8 @@ open Libnames
 open Nametab
 open Evd
 open Mod_subst
+open Misctypes
+open Decl_kinds
 
 let dl = dummy_loc
 
@@ -361,7 +363,8 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
       GCases (dl,tag,pred,[tomatch,(alias,aliastyp)],eqnl)
 
 let detype_sort = function
-  | Prop c -> GProp c
+  | Prop Null -> GProp
+  | Prop Pos -> GSet
   | Type u -> GType (Some u)
 
 type binder_kind = BProd | BLambda | BLetIn
@@ -391,7 +394,9 @@ let rec detype (isgoal:bool) avoid env t =
 	  GVar (dl, id))
     | Sort s -> GSort (dl,detype_sort s)
     | Cast (c1,k,c2) ->
-	GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
+        let d1 = detype isgoal avoid env c1 in
+	let d2 = detype isgoal avoid env c2 in
+	GCast(dl,d1,if k = VMcast then CastVM d2 else CastConv d2)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
@@ -668,14 +673,9 @@ let rec subst_glob_constr subst raw =
 		|Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _)) -> raw
 
   | GCast (loc,r1,k) ->
-      (match k with
-	   CastConv (k,r2) ->
-	     let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
-	       if r1' == r1 && r2' == r2 then raw else
-		 GCast (loc,r1', CastConv (k,r2'))
-	 | CastCoerce ->
-	     let r1' = subst_glob_constr subst r1 in
-	       if r1' == r1 then raw else GCast (loc,r1',k))
+      let r1' = subst_glob_constr subst r1 in
+      let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in
+      if r1' == r1 && k' == k then raw else GCast (loc,r1',k')
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index f9592194c..439609b02 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -15,6 +15,7 @@ open Environ
 open Glob_term
 open Termops
 open Mod_subst
+open Misctypes
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index ab11df450..e49f2b4eb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -662,7 +662,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
   | (id,_,c,cty,evsref,filter,occs)::subst ->
       let set_var k =
         match occs with
-        | Some (false,[]) -> mkVar id
+        | Some Locus.AllOccurrences -> mkVar id
         | Some _ -> error "Selection of specific occurrences not supported"
         | None ->
         let evty = set_holes evdref cty subst in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 3e2ca7aed..3d3760f18 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -13,6 +13,7 @@ open Environ
 open Termops
 open Reductionops
 open Evd
+open Locus
 
 (** returns exception Reduction.NotConvertible if not unifiable *)
 val the_conv_x     : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index fc1e1247f..466e73b8e 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -15,6 +15,9 @@ open Sign
 open Term
 open Libnames
 open Nametab
+open Decl_kinds
+open Misctypes
+open Locus
 (*i*)
 
 (* Untyped intermediate terms, after ASTs and before constr. *)
@@ -29,27 +32,6 @@ let cases_pattern_loc = function
     PatVar(loc,_) -> loc
   | PatCstr(loc,_,_,_) -> loc
 
-type patvar = identifier
-
-type glob_sort = GProp of Term.contents | GType of Univ.universe option
-
-type binding_kind = Lib.binding_kind = Explicit | Implicit
-
-type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
-
-type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-
-type 'a bindings =
-  | ImplicitBindings of 'a list
-  | ExplicitBindings of 'a explicit_bindings
-  | NoBindings
-
-type 'a with_bindings = 'a * 'a bindings
-
-type 'a cast_type =
-  | CastConv of cast_kind * 'a
-  | CastCoerce (* Cast to a base type (eg, an underlying inductive type) *)
-
 type glob_constr =
   | GRef of (loc * global_reference)
   | GVar of (loc * identifier)
@@ -142,7 +124,7 @@ let map_glob_constr_left_to_right f = function
       GRec (loc,fk,idl,comp1,comp2,comp3)
   | GCast (loc,c,k) -> 
       let comp1 = f c in
-      let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in
+      let comp2 = Miscops.map_cast_type f k in
       GCast (loc,comp1,comp2)
   | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
 
@@ -204,7 +186,7 @@ let fold_glob_constr f acc =
 	  (List.fold_left (fun acc (na,k,bbd,bty) ->
 	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
 	Array.fold_left fold (Array.fold_left fold acc tyl) bv
-    | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
+    | GCast (_,c,k) -> fold (match k with CastConv t | CastVM t -> fold acc t | CastCoerce -> acc) c
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
   and fold_pattern acc (_,idl,p,c) = fold acc c
@@ -243,7 +225,7 @@ let occur_glob_constr id =
                 (na=Name id or not(occur_fix bl)) in
           occur_fix bl)
           idl bl tyl bv)
-    | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
+    | GCast (loc,c,k) -> (occur c) or (match k with CastConv t | CastVM t -> occur t | CastCoerce -> false)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -301,7 +283,7 @@ let free_glob_vars  =
 	in
 	array_fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bounded vs c in
-	(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
+	(match k with CastConv t | CastVM t -> vars bounded v t | _ -> v)
     | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) =
@@ -380,17 +362,6 @@ type 'a glob_red_flag = {
 let all_flags =
   {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-
-type occurrences_expr = bool * int or_var list
-
-let all_occurrences_expr_but l = (false,l)
-let no_occurrences_expr_but l = (true,l)
-let all_occurrences_expr = (false,[])
-let no_occurrences_expr = (true,[])
-
-type 'a with_occurrences = occurrences_expr * 'a
-
 type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index d7d182833..f654925ef 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -19,6 +19,9 @@ open Sign
 open Term
 open Libnames
 open Nametab
+open Decl_kinds
+open Misctypes
+open Locus
 
 (**  The kind of patterns that occurs in "match ... with ... end"
 
@@ -30,27 +33,6 @@ type cases_pattern =
 
 val cases_pattern_loc : cases_pattern -> loc
 
-type patvar = identifier
-
-type glob_sort = GProp of Term.contents | GType of Univ.universe option
-
-type binding_kind = Lib.binding_kind = Explicit | Implicit
-
-type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
-
-type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-
-type 'a bindings =
-  | ImplicitBindings of 'a list
-  | ExplicitBindings of 'a explicit_bindings
-  | NoBindings
-
-type 'a with_bindings = 'a * 'a bindings
-
-type 'a cast_type =
-  | CastConv of cast_kind * 'a
-  | CastCoerce (** Cast to a base type (eg, an underlying inductive type) *)
-
 type glob_constr =
   | GRef of (loc * global_reference)
   | GVar of (loc * identifier)
@@ -137,17 +119,6 @@ type 'a glob_red_flag = {
 
 val all_flags : 'a glob_red_flag
 
-type 'a or_var = ArgArg of 'a | ArgVar of identifier located
-
-type occurrences_expr = bool * int or_var list
-
-val all_occurrences_expr_but : int or_var list -> occurrences_expr
-val no_occurrences_expr_but : int or_var list -> occurrences_expr
-val all_occurrences_expr : occurrences_expr
-val no_occurrences_expr : occurrences_expr
-
-type 'a with_occurrences = occurrences_expr * 'a
-
 type ('a,'b,'c) red_expr_gen =
   | Red of bool
   | Hnf
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
new file mode 100644
index 000000000..5f136c536
--- /dev/null
+++ b/pretyping/locusops.ml
@@ -0,0 +1,81 @@
+(************************************************************************)
+(*  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 *)
+
+let occurrences_map f = function
+  | OnlyOccurrences l ->
+    let l' = f l in
+    if l' = [] then NoOccurrences else OnlyOccurrences l'
+  | AllOccurrencesBut l ->
+    let l' = f l in
+    if l' = [] then AllOccurrences else AllOccurrencesBut l'
+  | (NoOccurrences|AllOccurrences) as o -> o
+
+let convert_occs = function
+  | AllOccurrences -> (false,[])
+  | AllOccurrencesBut l -> (false,l)
+  | NoOccurrences -> (true,[])
+  | OnlyOccurrences l -> (true,l)
+
+let is_selected occ = function
+  | AllOccurrences -> true
+  | AllOccurrencesBut l -> not (List.mem occ l)
+  | OnlyOccurrences l -> List.mem occ l
+  | NoOccurrences -> false
+
+(** Usual clauses *)
+
+let allHypsAndConcl = { onhyps=None; concl_occs=AllOccurrences }
+let allHyps = { onhyps=None; concl_occs=NoOccurrences }
+let onConcl = { onhyps=Some[]; concl_occs=AllOccurrences }
+let nowhere = { onhyps=Some[]; concl_occs=NoOccurrences }
+let onHyp h =
+  { onhyps=Some[(AllOccurrences,h),InHyp]; concl_occs=NoOccurrences }
+
+
+(** Clause conversion functions, parametrized by a hyp enumeration function *)
+
+(** From [clause] to [simple_clause] *)
+
+let simple_clause_of enum_hyps cl =
+  let error_occurrences () =
+    Errors.error "This tactic does not support occurrences selection" in
+  let error_body_selection () =
+    Errors.error "This tactic does not support body selection" in
+  let hyps =
+    match cl.onhyps with
+    | None ->
+	List.map Option.make (enum_hyps ())
+    | Some l ->
+	List.map (fun ((occs,id),w) ->
+	  if occs <> AllOccurrences then error_occurrences ();
+	  if w = InHypValueOnly then error_body_selection ();
+	  Some id) l in
+  if cl.concl_occs = NoOccurrences then hyps
+  else
+    if cl.concl_occs <> AllOccurrences then error_occurrences ()
+    else None :: hyps
+
+(** From [clause] to [concrete_clause] *)
+
+let concrete_clause_of enum_hyps cl =
+  let hyps =
+    match cl.onhyps with
+    | None ->
+	let f id = OnHyp (id,AllOccurrences,InHyp) in
+	List.map f (enum_hyps ())
+    | Some l ->
+	List.map (fun ((occs,id),w) -> OnHyp (id,occs,w)) l in
+  if cl.concl_occs = NoOccurrences then hyps
+  else
+    OnConcl cl.concl_occs :: hyps
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
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index ac0022c8c..6be95cd82 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -20,6 +20,7 @@ open Glob_term
 open Sign
 open Environ
 open Pattern
+open Misctypes
 (*i*)
 
 (* Given a term with second-order variables in it,
@@ -170,7 +171,9 @@ let matches_core convert allow_partial_app allow_bound_rels pat c =
 
       | PRel n1, Rel n2 when n1 = n2 -> subst
 
-      | PSort (GProp c1), Sort (Prop c2) when c1 = c2 -> subst
+      | PSort GProp, Sort (Prop Null) -> subst
+
+      | PSort GSet, Sort (Prop Pos) -> subst
 
       | PSort (GType _), Sort (Type _) -> subst
 
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
new file mode 100644
index 000000000..2528d57f3
--- /dev/null
+++ b/pretyping/miscops.ml
@@ -0,0 +1,43 @@
+(************************************************************************)
+(*  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 Misctypes
+open Pp
+open Nameops
+
+let map_cast_type f = function
+  | CastConv a -> CastConv (f a)
+  | CastVM a -> CastVM (f a)
+  | CastCoerce -> CastCoerce
+
+let smartmap_cast_type f c =
+  match c with
+    | CastConv a -> let a' = f a in if a' == a then c else CastConv a'
+    | CastVM a -> let a' = f a in if a' == a then c else CastVM a'
+    | CastCoerce -> CastCoerce
+
+(** Printing of [intro_pattern] *)
+
+let rec pr_intro_pattern (_,pat) = match pat with
+  | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
+  | IntroWildcard -> str "_"
+  | IntroRewrite true -> str "->"
+  | IntroRewrite false -> str "<-"
+  | IntroIdentifier id -> pr_id id
+  | IntroFresh id -> str "?" ++ pr_id id
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
+  | IntroAnonymous -> str "?"
+
+and pr_or_and_intro_pattern = function
+  | [pl] ->
+      str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
+  | pll ->
+      str "[" ++
+      hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+      ++ str "]"
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
new file mode 100644
index 000000000..b8f6f6860
--- /dev/null
+++ b/pretyping/miscops.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(*  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 Misctypes
+
+val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
+
+val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
+
+(** Printing of [intro_pattern] *)
+
+val pr_intro_pattern : intro_pattern_expr Pp.located -> Pp.std_ppcmds
+val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 47cc57fd1..ef81aa4d3 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -17,6 +17,8 @@ open Environ
 open Nametab
 open Pp
 open Mod_subst
+open Misctypes
+open Decl_kinds
 
 (* Metavariables *)
 
@@ -100,7 +102,8 @@ let pattern_of_constr sigma t =
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (id_of_string ("META" ^ string_of_int n)))
     | Var id -> PVar id
-    | Sort (Prop c) -> PSort (GProp c)
+    | Sort (Prop Null) -> PSort GProp
+    | Sort (Prop Pos) -> PSort GSet
     | Sort (Type _) -> PSort (GType None)
     | Cast (c,_,_)      -> pattern_of_constr c
     | LetIn (na,c,_,b) -> PLetIn (na,pattern_of_constr c,pattern_of_constr b)
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index e6ec9a498..f9c2358b7 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -18,6 +18,7 @@ open Libnames
 open Nametab
 open Glob_term
 open Mod_subst
+open Misctypes
 
 (** {5 Maps of pattern variables} *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index d2553828f..82f030ae0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -44,6 +44,7 @@ open Pretype_errors
 open Glob_term
 open Evarconv
 open Pattern
+open Misctypes
 
 type typing_constraint = OfType of types option | IsType
 type var_map = (identifier * constr_under_binders) list
@@ -95,12 +96,13 @@ let ((constr_in : constr -> Dyn.t),
 (** Miscellaneous interpretation functions *)
 
 let interp_sort = function
-  | GProp c -> Prop c
+  | GProp -> Prop Null
+  | GSet -> Prop Pos
   | GType _ -> new_Type_sort ()
 
 let interp_elimination_sort = function
-  | GProp Null -> InProp
-  | GProp Pos  -> InSet
+  | GProp -> InProp
+  | GSet  -> InSet
   | GType _ -> InType
 
 let resolve_evars env evdref fail_evar resolve_classes =
@@ -239,7 +241,8 @@ let pretype_ref evdref env ref =
     make_judge c (Retyping.get_type_of env Evd.empty c)
 
 let pretype_sort evdref = function
-  | GProp c -> judge_of_prop_contents c
+  | GProp -> judge_of_prop
+  | GSet -> judge_of_set
   | GType _ -> evd_comb0 judge_of_new_Type evdref
 
 exception Found of fixpoint
@@ -474,7 +477,7 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
   | GLetIn(loc,name,c1,c2)      ->
       let j =
 	match c1 with
-	| GCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	| GCast (loc, c, CastConv t) ->
 	    let tj = pretype_type empty_valcon env evdref lvar t in
 	      pretype (mk_tycon tj.utj_val) env evdref lvar c
 	| _ -> pretype empty_tycon env evdref lvar c1
@@ -632,7 +635,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 	| CastCoerce ->
 	  let cj = pretype empty_tycon env evdref lvar c in
 	    evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
-	| CastConv (k,t) ->
+	| CastConv t | CastVM t ->
+	  let k = (match k with CastVM _ -> VMcast | _ -> DEFAULTcast) in
 	  let tj = pretype_type empty_valcon env evdref lvar t in
 	  let tval = nf_evar !evdref tj.utj_val in
 	  let cj = match k with
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 75e507afd..9401edc2d 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -19,6 +19,7 @@ open Environ
 open Evd
 open Glob_term
 open Evarutil
+open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 199adf6a7..e520602db 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,3 +1,4 @@
+Locusops
 Termops
 Evd
 Reductionops
@@ -13,6 +14,7 @@ Recordops
 Evarconv
 Arguments_renaming
 Typing
+Miscops
 Glob_term
 Pattern
 Matching
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index cc1f6f941..6ff469012 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -25,6 +25,7 @@ open Cbv
 open Glob_term
 open Pattern
 open Matching
+open Locus
 
 (* Errors *)
 
@@ -842,7 +843,8 @@ let matches_head c t =
     | App (f,_) -> matches c f
     | _ -> raise PatternMatchingFailure
 
-let contextually byhead ((nowhere_except_in,locs),c) f env sigma t =
+let contextually byhead (occs,c) f env sigma t =
+  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref 1 in
   let rec traverse (env,c as envc) t =
@@ -913,15 +915,20 @@ let unfold env sigma name =
  * Unfolds the constant name in a term c following a list of occurrences occl.
  * at the occurrences of occ_list. If occ_list is empty, unfold all occurences.
  * Performs a betaiota reduction after unfolding. *)
-let unfoldoccs env sigma ((nowhere_except_in,locs as plocs),name) c =
-  if locs = [] then if nowhere_except_in then c else unfold env sigma name c
-  else
-    let (nbocc,uc) = substlin env name 1 plocs c in
+let unfoldoccs env sigma (occs,name) c =
+  let unfo nowhere_except_in locs =
+    let (nbocc,uc) = substlin env name 1 (nowhere_except_in,locs) c in
     if nbocc = 1 then
       error ((string_of_evaluable_ref env name)^" does not occur.");
     let rest = List.filter (fun o -> o >= nbocc) locs in
     if rest <> [] then error_invalid_occurrence rest;
     nf_betaiotazeta sigma uc
+  in
+  match occs with
+    | NoOccurrences -> c
+    | AllOccurrences -> unfold env sigma name c
+    | OnlyOccurrences l -> unfo true l
+    | AllOccurrencesBut l -> unfo false l
 
 (* Unfold reduction tactic: *)
 let unfoldn loccname env sigma c =
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 8fd14dccb..c9b139ac9 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -16,6 +16,7 @@ open Glob_term
 open Termops
 open Pattern
 open Libnames
+open Locus
 
 type reduction_tactic_error =
     InvalidAbstraction of env * constr * (env * Type_errors.type_error)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index f64625707..a9cb72504 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -16,6 +16,7 @@ open Sign
 open Environ
 open Libnames
 open Nametab
+open Locus
 
 (* Sorts and sort family *)
 
@@ -692,15 +693,6 @@ let replace_term = replace_term_gen eq_constr
    occurrence except the ones in l and b=false, means all occurrences
    except the ones in l *)
 
-type hyp_location_flag = (* To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
-type occurrences = bool * int list
-let all_occurrences = (false,[])
-let no_occurrences_in_set = (true,[])
-
 let error_invalid_occurrence l =
   let l = list_uniquize (List.sort Pervasives.compare l) in
   errorlabstrm ""
@@ -715,7 +707,7 @@ let pr_position (cl,pos) =
     | Some (id,InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in
   int pos ++ clpos
 
-let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_except_in,locs) =
+let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) =
   let s = if nested then "Found nested occurrences of the pattern"
     else "Found incompatible occurrences of the pattern" in
   errorlabstrm ""
@@ -726,10 +718,6 @@ let error_cannot_unify_occurrences nested (cl2,pos2,t2) (cl1,pos1,t1) (nowhere_e
      quote (print_constr t1) ++ strbrk " at position " ++ 
      pr_position (cl1,pos1) ++ str ".")
 
-let is_selected pos (nowhere_except_in,locs) =
-  nowhere_except_in && List.mem pos locs ||
-  not nowhere_except_in && not (List.mem pos locs)
-
 exception NotUnifiable
 
 type 'a testing_function = {
@@ -739,7 +727,8 @@ type 'a testing_function = {
   mutable last_found : ((identifier * hyp_location_flag) option * int * constr) option
 }
 
-let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl occ t =
+let subst_closed_term_occ_gen_modulo occs test cl occ t =
+  let (nowhere_except_in,locs) = Locusops.convert_occs occs in
   let maxocc = List.fold_right max locs 0 in
   let pos = ref occ in
   let nested = ref false in
@@ -749,12 +738,12 @@ let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl o
       test.last_found <- Some (cl,!pos,t)
     with NotUnifiable ->
       let lastpos = Option.get test.last_found in
-      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos plocs in
+      error_cannot_unify_occurrences !nested (cl,!pos,t) lastpos in
   let rec substrec k t =
     if nowhere_except_in & !pos > maxocc then t else
     try
       let subst = test.match_fun t in
-      if is_selected !pos plocs then
+      if Locusops.is_selected !pos occs then
         (add_subst t subst; incr pos;
          (* Check nested matching subterms *)
          nested := true; ignore (subst_below k t); nested := false;
@@ -770,15 +759,15 @@ let subst_closed_term_occ_gen_modulo (nowhere_except_in,locs as plocs) test cl o
   let t' = substrec 1 t in
   (!pos, t')
 
-let is_nowhere (nowhere_except_in,locs) = nowhere_except_in && locs = [] 
-
 let check_used_occurrences nbocc (nowhere_except_in,locs) =
   let rest = List.filter (fun o -> o >= nbocc) locs in
   if rest <> [] then error_invalid_occurrence rest
 
-let proceed_with_occurrences f plocs x =
-  if is_nowhere plocs then (* optimization *) x else
-  begin
+let proceed_with_occurrences f occs x =
+  if occs = NoOccurrences then x
+  else begin
+    (* TODO FINISH ADAPTING WITH HUGO *)
+    let plocs = Locusops.convert_occs occs in
     assert (List.for_all (fun x -> x >= 0) (snd plocs));
     let (nbocc,x) = f 1 x in
     check_used_occurrences nbocc plocs;
@@ -792,16 +781,17 @@ let make_eq_test c = {
   last_found = None
 } 
 
-let subst_closed_term_occ_gen plocs pos c t =
-  subst_closed_term_occ_gen_modulo plocs (make_eq_test c) None pos t
+let subst_closed_term_occ_gen occs pos c t =
+  subst_closed_term_occ_gen_modulo occs (make_eq_test c) None pos t
 
-let subst_closed_term_occ plocs c t =
-  proceed_with_occurrences (fun occ -> subst_closed_term_occ_gen plocs occ c)
-    plocs t
+let subst_closed_term_occ occs c t =
+  proceed_with_occurrences
+    (fun occ -> subst_closed_term_occ_gen occs occ c)
+    occs t
 
-let subst_closed_term_occ_modulo plocs test cl t =
+let subst_closed_term_occ_modulo occs test cl t =
   proceed_with_occurrences
-    (subst_closed_term_occ_gen_modulo plocs test cl) plocs t
+    (subst_closed_term_occ_gen_modulo occs test cl) occs t
 
 let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) =
   let f = f (Some (id,hyploc)) in
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 68db293b6..e5dc2448b 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -13,6 +13,7 @@ open Names
 open Term
 open Sign
 open Environ
+open Locus
 
 (** Universes *)
 val new_univ_level : unit -> Univ.universe_level
@@ -145,11 +146,6 @@ val subst_term : constr -> constr -> constr
 (** [replace_term d e c] replaces [d] by [e] in [c] *)
 val replace_term : constr -> constr -> constr -> constr
 
-(** In occurrences sets, false = everywhere except and true = nowhere except *)
-type occurrences = bool * int list
-val all_occurrences : occurrences
-val no_occurrences_in_set : occurrences
-
 (** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at
    positions [occl], counting from [n], by [Rel 1] in [d] *)
 val subst_closed_term_occ_gen :
@@ -161,11 +157,6 @@ val subst_closed_term_occ_gen :
     failing with NotUnifiable) and an initial substitution are
     required too *)
 
-type hyp_location_flag = (** To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
 type 'a testing_function = {
   match_fun : constr -> 'a;
   merge_fun : 'a -> 'a -> 'a;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2344f6e46..fd40cca7c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -25,6 +25,7 @@ open Pretype_errors
 open Retyping
 open Coercion
 open Recordops
+open Locus
 
 let occur_meta_or_undefined_evar evd c =
   let rec occrec c = match kind_of_term c with
@@ -56,7 +57,7 @@ let abstract_scheme env c l lname_typ =
 
 let abstract_list_all env evd typ c l =
   let ctxt,_ = splay_prod_n env evd (List.length l) typ in
-  let l_with_all_occs = List.map (function a -> (all_occurrences,a)) l in
+  let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in
   let p = abstract_scheme env c l_with_all_occs ctxt in
   try
     if is_conv_leq env evd (Typing.type_of env evd p) typ then p
@@ -65,7 +66,7 @@ let abstract_list_all env evd typ c l =
     error_cannot_find_well_typed_abstraction env evd p l
 
 let set_occurrences_of_last_arg args =
-  Some all_occurrences :: List.tl (array_map_to_list (fun _ -> None) args)
+  Some AllOccurrences :: List.tl (array_map_to_list (fun _ -> None) args)
 
 let abstract_list_all_with_dependencies env evd typ c l =
   let evd,ev = new_evar evd env typ in