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

17 files changed, 144 insertions, 113 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 06d922a7c..c8ca6cbab 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -18,6 +18,8 @@ open Topconstr
 open Util
 open Tok
 open Compat
+open Misctypes
+open Decl_kinds
 
 let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
@@ -29,7 +31,7 @@ let _ = List.iter Lexer.add_keyword constr_kw
 
 let mk_cast = function
     (c,(_,None)) -> c
-  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv (DEFAULTcast, ty))
+  | (c,(_,Some ty)) -> CCast(join_loc (constr_loc c) (constr_loc ty), c, CastConv ty)
 
 let binders_of_names l =
   List.map (fun (loc, na) ->
@@ -38,7 +40,7 @@ let binders_of_names l =
 
 let binders_of_lidents l =
   List.map (fun (loc, id) ->
-    LocalRawAssum ([loc, Name id], Default Glob_term.Explicit,
+    LocalRawAssum ([loc, Name id], Default Explicit,
 		  CHole (loc, Some (Evar_kinds.BinderType (Name id))))) l
 
 let mk_fixb (id,bl,ann,body,(loc,tyc)) =
@@ -144,8 +146,8 @@ GEXTEND Gram
     [ [ c = lconstr -> c ] ]
   ;
   sort:
-    [ [ "Set"  -> GProp Pos
-      | "Prop" -> GProp Null
+    [ [ "Set"  -> GSet
+      | "Prop" -> GProp
       | "Type" -> GType None ] ]
   ;
   lconstr:
@@ -160,13 +162,13 @@ GEXTEND Gram
       [ c = binder_constr -> c ]
     | "100" RIGHTA
       [ c1 = operconstr; "<:"; c2 = binder_constr ->
-                 CCast(loc,c1, CastConv (VMcast,c2))
+                 CCast(loc,c1, CastVM c2)
       | c1 = operconstr; "<:"; c2 = SELF ->
-                 CCast(loc,c1, CastConv (VMcast,c2))
+                 CCast(loc,c1, CastVM c2)
       | c1 = operconstr; ":";c2 = binder_constr ->
-                 CCast(loc,c1, CastConv (DEFAULTcast,c2))
+                 CCast(loc,c1, CastConv c2)
       | c1 = operconstr; ":"; c2 = SELF ->
-                 CCast(loc,c1, CastConv (DEFAULTcast,c2))
+                 CCast(loc,c1, CastConv c2)
       | c1 = operconstr; ":>" ->
                  CCast(loc,c1, CastCoerce) ]
     | "99" RIGHTA [ ]
@@ -410,7 +412,7 @@ GEXTEND Gram
       | "("; id=name; ":="; c=lconstr; ")" ->
           [LocalRawDef (id,c)]
       | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" ->
-          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))]
+          [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv t))]
       | "{"; id=name; "}" ->
           [LocalRawAssum ([id],Default Implicit,CHole (loc, None))]
       | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" ->
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index bf0e13e02..e2edbb096 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -17,6 +17,7 @@ open Pcoq
 open Prim
 open Tactic
 open Tok
+open Misctypes
 
 let fail_default_value = ArgArg 0
 
@@ -177,7 +178,7 @@ GEXTEND Gram
 	  let t, ty =
 	    match mpv with
 	    | Term t -> (match t with
-	      | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty)
+	      | CCast (loc, t, (CastConv ty | CastVM ty)) -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
 	  in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index fd6fc7dd8..d6b2d8380 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -86,8 +86,8 @@ GEXTEND Gram
     [ [ s = ne_string; sc = OPT ["%"; key = IDENT -> key ] -> (loc,s,sc) ] ]
   ;
   smart_global:
-    [ [ c = reference -> Genarg.AN c
-      | ntn = by_notation -> Genarg.ByNotation ntn ] ]
+    [ [ c = reference -> Misctypes.AN c
+      | ntn = by_notation -> Misctypes.ByNotation ntn ] ]
   ;
   qualid:
     [ [ qid = basequalid -> loc, qid ] ]
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5f44a9e9c..6edb0bfc1 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -17,6 +17,7 @@ open Locality
 open Prim
 open Constr
 open Tok
+open Misctypes
 
 let thm_token = G_vernac.thm_token
 
@@ -113,6 +114,6 @@ GEXTEND Gram
     ;
   constr_body:
     [ [ ":="; c = lconstr -> c
-      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c, Glob_term.CastConv (Term.DEFAULTcast,t)) ] ]
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,CastConv t) ] ]
   ;
 END
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 8b72a5e93..7cbcd584c 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -18,6 +18,9 @@ open Libnames
 open Termops
 open Tok
 open Compat
+open Misctypes
+open Locus
+open Decl_kinds
 
 let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta]
 
@@ -166,17 +169,17 @@ let mkCLambdaN_simple bl c =
 let loc_of_ne_list l = join_loc (fst (List.hd l)) (fst (list_last l))
 
 let map_int_or_var f = function
-  | Glob_term.ArgArg x -> Glob_term.ArgArg (f x)
-  | Glob_term.ArgVar _ as y -> y
+  | ArgArg x -> ArgArg (f x)
+  | ArgVar _ as y -> y
 
-let all_concl_occs_clause = { onhyps=Some[]; concl_occs=all_occurrences_expr }
+let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
 
 let has_no_specified_occs cl =
   (cl.onhyps = None || 
-    List.for_all (fun ((occs,_),_) -> occs = all_occurrences_expr)
+    List.for_all (fun ((occs,_),_) -> occs = AllOccurrences)
     (Option.get cl.onhyps))
-  && (cl.concl_occs = all_occurrences_expr 
-      || cl.concl_occs = no_occurrences_expr)
+  && (cl.concl_occs = AllOccurrences
+      || cl.concl_occs = NoOccurrences)
 
 let merge_occurrences loc cl = function
   | None ->
@@ -185,11 +188,11 @@ let merge_occurrences loc cl = function
 	user_err_loc (loc,"",str "Found an \"at\" clause without \"with\" clause.")
   | Some (occs,p) ->
       (Some p,
-      if occs = all_occurrences_expr then cl
+      if occs = AllOccurrences then cl
       else if cl = all_concl_occs_clause then { onhyps=Some[]; concl_occs=occs }
       else match cl.onhyps with
       | Some [(occs',id),l] when
-	  occs' = all_occurrences_expr && cl.concl_occs = no_occurrences_expr ->
+	  occs' = AllOccurrences && cl.concl_occs = NoOccurrences ->
 	  { cl with onhyps=Some[(occs,id),l] }
       | _ ->
 	  if has_no_specified_occs cl then
@@ -205,12 +208,12 @@ GEXTEND Gram
   simple_intropattern;
 
   int_or_var:
-    [ [ n = integer  -> Glob_term.ArgArg n
-      | id = identref -> Glob_term.ArgVar id ] ]
+    [ [ n = integer  -> ArgArg n
+      | id = identref -> ArgVar id ] ]
   ;
   nat_or_var:
-    [ [ n = natural  -> Glob_term.ArgArg n
-      | id = identref -> Glob_term.ArgVar id ] ]
+    [ [ n = natural  -> ArgArg n
+      | id = identref -> ArgVar id ] ]
   ;
   (* An identifier or a quotation meta-variable *)
   id_or_meta:
@@ -236,18 +239,18 @@ GEXTEND Gram
   ;
   conversion:
     [ [ c = constr -> (None, c)
-      | c1 = constr; "with"; c2 = constr -> (Some (all_occurrences_expr,c1),c2)
+      | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2)
       | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr ->
           (Some (occs,c1), c2) ] ]
   ;
   occs_nums:
-    [ [ nl = LIST1 nat_or_var -> no_occurrences_expr_but nl
+    [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl
       | "-"; n = nat_or_var; nl = LIST0 int_or_var ->
 	  (* have used int_or_var instead of nat_or_var for compatibility *)
-	   all_occurrences_expr_but (List.map (map_int_or_var abs) (n::nl)) ] ]
+	   AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ]
   ;
   occs:
-    [ [ "at"; occs = occs_nums -> occs | -> all_occurrences_expr ] ]
+    [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ]
   ;
   pattern_occ:
     [ [ c = constr; nl = occs -> (nl,c) ] ]
@@ -374,7 +377,7 @@ GEXTEND Gram
       | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ ->
           {onhyps=Some hl; concl_occs=occs}
       | hl=LIST0 hypident_occ SEP"," ->
-          {onhyps=Some hl; concl_occs=no_occurrences_expr} ] ]
+          {onhyps=Some hl; concl_occs=NoOccurrences} ] ]
   ;
   clause_dft_concl:
     [ [ "in"; cl = in_clause -> cl
@@ -383,14 +386,14 @@ GEXTEND Gram
   ;
   clause_dft_all:
     [ [ "in"; cl = in_clause -> cl
-      | -> {onhyps=None; concl_occs=all_occurrences_expr} ] ]
+      | -> {onhyps=None; concl_occs=AllOccurrences} ] ]
   ;
   opt_clause:
     [ [ "in"; cl = in_clause -> Some cl | -> None ] ]
   ;
   concl_occ:
     [ [ "*"; occs = occs -> occs
-      | -> no_occurrences_expr ] ]
+      | -> NoOccurrences ] ]
   ;
   in_hyp_list:
     [ [ "in"; idl = LIST1 id_or_meta -> idl
@@ -546,9 +549,9 @@ GEXTEND Gram
 	  TacMutualCofix (false,id,List.map mk_cofix_tac fd)
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacLetTac (Names.Name id,b,nowhere,true)
+	  TacLetTac (Names.Name id,b,Locusops.nowhere,true)
       | IDENT "pose"; b = constr; na = as_name ->
-	  TacLetTac (na,b,nowhere,true)
+	  TacLetTac (na,b,Locusops.nowhere,true)
       | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
 	  TacLetTac (Names.Name id,c,p,true)
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
@@ -572,9 +575,9 @@ GEXTEND Gram
 
       | IDENT "cut"; c = constr -> TacCut c
       | IDENT "generalize"; c = constr ->
-	  TacGeneralize [((all_occurrences_expr,c),Names.Anonymous)]
+	  TacGeneralize [((AllOccurrences,c),Names.Anonymous)]
       | IDENT "generalize"; c = constr; l = LIST1 constr ->
-	  let gen_everywhere c = ((all_occurrences_expr,c),Names.Anonymous) in
+	  let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
           TacGeneralize (List.map gen_everywhere (c::l))
       | IDENT "generalize"; c = constr; lookup_at_as_coma; nl = occs;
           na = as_name;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f684b9a0d..34e0d9532 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -23,6 +23,7 @@ open Genarg
 open Ppextend
 open Goptions
 open Declaremods
+open Misctypes
 
 open Prim
 open Constr
@@ -240,7 +241,7 @@ GEXTEND Gram
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
       (match c with
-          CCast(_,c, Glob_term.CastConv (Term.DEFAULTcast,t)) -> DefineBody (bl, red, c, Some t)
+          CCast(_,c, CastConv t) -> DefineBody (bl, red, c, Some t)
         | _ -> DefineBody (bl, red, c, None))
     | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr ->
 	DefineBody (bl, red, c, Some t)
@@ -343,7 +344,7 @@ GEXTEND Gram
 	   (oc,DefExpr (id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
       | l = binders; ":="; b = lconstr -> fun id ->
          match b with
-	 | CCast(_,b, Glob_term.CastConv (_, t)) ->
+	 | CCast(_,b, (CastConv t|CastVM t)) ->
 	     (None,DefExpr(id,mkCLambdaN loc l b,Some (mkCProdN loc l t)))
          | _ ->
 	     (None,DefExpr(id,mkCLambdaN loc l b,None)) ] ]
@@ -568,7 +569,7 @@ GEXTEND Gram
 	  VernacContext c
 
       | IDENT "Instance"; namesup = instance_name; ":";
-	 expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200";
+	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ;
 	 props = [ ":="; "{"; r = record_declaration; "}" -> Some r |
 	     ":="; c = lconstr -> Some c | -> None ] ->
@@ -714,7 +715,7 @@ GEXTEND Gram
 
       (* Hack! Should be in grammar_ext, but camlp4 factorize badly *)
       | IDENT "Declare"; IDENT "Instance"; namesup = instance_name; ":";
-	 expl = [ "!" -> Glob_term.Implicit | -> Glob_term.Explicit ] ; t = operconstr LEVEL "200";
+	 expl = [ "!" -> Decl_kinds.Implicit | -> Decl_kinds.Explicit ] ; t = operconstr LEVEL "200";
 	 pri = OPT [ "|"; i = natural -> i ] ->
 	   VernacInstance (true, not (use_section_locality ()),
 			   snd namesup, (fst namesup, expl, t),
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 3cb553437..7c26ac124 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -20,6 +20,8 @@ open Libnames
 open Nametab
 open Detyping
 open Tok
+open Misctypes
+open Decl_kinds
 
 (* Generic xml parser without raw data *)
 
@@ -96,8 +98,8 @@ let inductive_of_cdata a = match global_of_cdata a with
 let ltacref_of_cdata (loc,a) = (loc,locate_tactic (uri_of_data a))
 
 let sort_of_cdata (loc,a) = match a with
-  | "Prop" -> GProp Null
-  | "Set" -> GProp Pos
+  | "Prop" -> GProp
+  | "Set" -> GSet
   | "Type" -> GType None
   | _ -> user_err_loc (loc,"",str "sort expected.")
 
@@ -191,7 +193,7 @@ let rec interp_xml_constr = function
       let ln,lc,lt = list_split3 (List.map interp_xml_CoFixFunction xl) in
       GRec (loc, GCoFix (get_xml_noFun al), Array.of_list ln, [||], Array.of_list lc, Array.of_list lt)
   | XmlTag (loc,"CAST",al,[x1;x2]) ->
-      GCast (loc, interp_xml_term x1, CastConv (DEFAULTcast, interp_xml_type x2))
+      GCast (loc, interp_xml_term x1, CastConv (interp_xml_type x2))
   | XmlTag (loc,"SORT",al,[]) ->
       GSort (loc, get_xml_sort al)
   | XmlTag (loc,s,_,_) ->
diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib
index 39fd88506..cae4b13d6 100644
--- a/parsing/grammar.mllib
+++ b/parsing/grammar.mllib
@@ -56,11 +56,13 @@ Lib
 Goptions
 Decl_kinds
 Global
+Locusops
 Termops
 Namegen
 Evd
 Reductionops
 Inductiveops
+Miscops
 Glob_term
 Detyping
 Pattern
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index ebcc53264..5bc6bddd9 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -17,6 +17,7 @@ open Topconstr
 open Tacexpr
 open Libnames
 open Compat
+open Misctypes
 
 (** The parser of Coq *)
 
@@ -220,7 +221,7 @@ module Tactic :
     val int_or_var : int or_var Gram.entry
     val red_expr : raw_red_expr Gram.entry
     val simple_tactic : raw_atomic_tactic_expr Gram.entry
-    val simple_intropattern : Genarg.intro_pattern_expr located Gram.entry
+    val simple_intropattern : intro_pattern_expr located Gram.entry
     val tactic_arg : raw_tactic_arg Gram.entry
     val tactic_expr : raw_tactic_expr Gram.entry
     val binder_tactic : raw_tactic_expr Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 98ed6883e..45ea77d13 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -21,6 +21,9 @@ open Pattern
 open Glob_term
 open Constrextern
 open Termops
+open Decl_kinds
+open Misctypes
+open Locus
 (*i*)
 
 let sep_v = fun _ -> str"," ++ spc()
@@ -110,8 +113,8 @@ let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)"
 let pr_universe = Univ.pr_uni
 
 let pr_glob_sort = function
-  | GProp Term.Null -> str "Prop"
-  | GProp Term.Pos -> str "Set"
+  | GProp -> str "Prop"
+  | GSet -> str "Set"
   | GType u -> hov 0 (str "Type" ++ pr_opt (pr_in_comment pr_universe) u)
 
 let pr_id = pr_id
@@ -253,7 +256,7 @@ let pr_binder_among_many pr_c = function
       pr_binder true pr_c (nal,k,t)
   | LocalRawDef (na,c) ->
       let c,topt = match c with
-        | CCast(_,c, CastConv (_,t)) -> c, t
+        | CCast(_,c, (CastConv t|CastVM t)) -> c, t
         | _ -> c, CHole (dummy_loc, None) in
       surround (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
@@ -530,13 +533,12 @@ let pr pr sep inherited a =
   | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_glob_sort s, latom
-  | CCast (_,a,CastConv (k,b)) ->
-      let s = match k with VMcast -> "<:" | DEFAULTcast | REVERTcast -> ":" in
-      hv 0 (pr mt (lcast,L) a ++ cut () ++ str s ++ pr mt (-lcast,E) b),
-      lcast
-  | CCast (_,a,CastCoerce) ->
-      hv 0 (pr mt (lcast,L) a ++ cut () ++ str ":>"),
-      lcast
+  | CCast (_,a,b) ->
+      hv 0 (pr mt (lcast,L) a ++ cut () ++
+	    match b with
+	      | CastConv b -> str ":" ++ pr mt (-lcast,E) b
+	      | CastVM b -> str "<:" ++ pr mt (-lcast,E) b
+	      | CastCoerce -> str ":>"), lcast
   | CNotation (_,"( _ )",([t],[],[])) ->
       pr (fun()->str"(") (max_int,L) t ++ str")", latom
   | CNotation (_,s,env) ->
@@ -581,12 +583,15 @@ let pr_cases_pattern_expr = pr_patt ltop
 
 let pr_binders = pr_undelimited_binders spc (pr ltop)
 
-let pr_with_occurrences pr occs =
+let pr_with_occurrences pr (occs,c) =
   match occs with
-    ((false,[]),c) -> pr c
-  | ((nowhere_except_in,nl),c) ->
+    | AllOccurrences -> pr c
+    | NoOccurrences -> failwith "pr_with_occurrences: no occurrences"
+    | OnlyOccurrences nl ->
       hov 1 (pr c ++ spc() ++ str"at " ++
-        (if nowhere_except_in then mt() else str "- ") ++
+        hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+    | AllOccurrencesBut nl ->
+      hov 1 (pr c ++ spc() ++ str"at - " ++
         hov 0 (prlist_with_sep spc (pr_or_var int) nl))
 
 let pr_red_flag pr r =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index c61d4c206..1497c90e7 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -16,7 +16,8 @@ open Topconstr
 open Names
 open Errors
 open Util
-open Genarg
+open Misctypes
+open Locus
 
 val extract_lam_binders :
   constr_expr -> local_binder list * constr_expr
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 513034194..c50ab9fcd 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -20,6 +20,9 @@ open Pattern
 open Ppextend
 open Ppconstr
 open Printer
+open Misctypes
+open Locus
+open Decl_kinds
 
 let pr_global x = Nametab.pr_global_env Idset.empty x
 
@@ -384,11 +387,11 @@ let pr_by_tactic prt = function
   | tac -> spc() ++ str "by " ++ prt tac
 
 let pr_hyp_location pr_id = function
-  | occs, Termops.InHyp -> spc () ++ pr_with_occurrences pr_id occs
-  | occs, Termops.InHypTypeOnly ->
+  | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+  | occs, InHypTypeOnly ->
       spc () ++
       pr_with_occurrences (fun id -> str "(type of " ++ pr_id id ++ str ")") occs
-  | occs, Termops.InHypValueOnly ->
+  | occs, InHypValueOnly ->
       spc () ++
       pr_with_occurrences (fun id -> str "(value of " ++ pr_id id ++ str ")") occs
 
@@ -403,17 +406,17 @@ let pr_in_hyp_as pr_id = function
   | Some (id,ipat) -> pr_simple_hyp_clause pr_id [id] ++ pr_as_ipat ipat
 
 let pr_clauses default_is_concl pr_id = function
-  | { onhyps=Some []; concl_occs=occs }
-      when occs = all_occurrences_expr & default_is_concl = Some true -> mt ()
-  | { onhyps=None; concl_occs=occs }
-      when occs = all_occurrences_expr & default_is_concl = Some false -> mt ()
+  | { onhyps=Some []; concl_occs=AllOccurrences }
+      when default_is_concl = Some true -> mt ()
+  | { onhyps=None; concl_occs=AllOccurrences }
+      when default_is_concl = Some false -> mt ()
   | { onhyps=None; concl_occs=occs } ->
-      if occs = no_occurrences_expr then pr_in (str " * |-")
+      if occs = NoOccurrences then pr_in (str " * |-")
       else pr_in (pr_with_occurrences (fun () -> str " *") (occs,()))
   | { onhyps=Some l; concl_occs=occs } ->
       pr_in
         (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++
-	 (if occs = no_occurrences_expr then mt ()
+	 (if occs = NoOccurrences then mt ()
 	  else pr_with_occurrences (fun () -> str" |- *") (occs,())))
 
 let pr_orient b = if b then mt () else str " <-"
@@ -690,7 +693,7 @@ and pr_atom1 = function
   | TacGeneralizeDep c ->
       hov 1 (str "generalize" ++ spc () ++ str "dependent" ++
              pr_constrarg c)
-  | TacLetTac (na,c,cl,true) when cl = nowhere ->
+  | TacLetTac (na,c,cl,true) when cl = Locusops.nowhere ->
       hov 1 (str "pose" ++ pr_pose pr_lconstr pr_constr na c)
   | TacLetTac (na,c,cl,b) ->
       hov 1 ((if b then str "set" else str "remember") ++
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index d85f1ec3f..afcc83c68 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -17,6 +17,7 @@ open Pattern
 open Ppextend
 open Environ
 open Evd
+open Misctypes
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index fad4e879e..5dbef1fe5 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -31,6 +31,7 @@ open Printmod
 open Libnames
 open Nametab
 open Recordops
+open Misctypes
 
 type object_pr = {
   print_inductive           : mutual_inductive -> std_ppcmds;
@@ -644,11 +645,11 @@ let print_any_name = function
       "print_name" (pr_qualid qid ++ spc () ++ str "not a defined object.")
 
 let print_name = function
-  | Genarg.ByNotation (loc,ntn,sc) ->
+  | ByNotation (loc,ntn,sc) ->
       print_any_name
         (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
                ntn sc))
-  | Genarg.AN ref ->
+  | AN ref ->
       print_any_name (locate_any_name ref)
 
 let print_opaque_name qid =
@@ -686,11 +687,11 @@ let print_about_any k =
       hov 0 (pr_located_qualid k) ++ fnl()
 
 let print_about = function
-  | Genarg.ByNotation (loc,ntn,sc) ->
+  | ByNotation (loc,ntn,sc) ->
       print_about_any
         (Term (Notation.interp_notation_as_global_reference loc (fun _ -> true)
                ntn sc))
-  | Genarg.AN ref ->
+  | AN ref ->
       print_about_any (locate_any_name ref)
 
 (* for debug *)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 40ba7f047..b3271d141 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -16,7 +16,7 @@ open Environ
 open Reductionops
 open Libnames
 open Nametab
-open Genarg
+open Misctypes
 
 (** A Pretty-Printer for the Calculus of Inductive Constructions. *)
 
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index f5225feb3..543240a82 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -17,6 +17,7 @@ open Pp
 open Compat
 open Pcaml
 open PcamlSig
+open Misctypes
 
 let loc = dummy_loc
 let dloc = <:expr< Pp.dummy_loc >>
@@ -33,8 +34,8 @@ EXTEND
       <:expr< snd (Pattern.pattern_of_glob_constr $c$) >> ] ]
   ;
   sort:
-    [ [ "Set"  -> GProp Pos
-      | "Prop" -> GProp Null
+    [ [ "Set"  -> GSet
+      | "Prop" -> GProp
       | "Type" -> GType None ] ]
   ;
   ident:
@@ -49,9 +50,9 @@ EXTEND
   constr:
     [ "200" RIGHTA
       [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
-        <:expr< Glob_term.GProd ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >>
+        <:expr< Glob_term.GProd ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
       | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
-        <:expr< Glob_term.GLambda ($dloc$,Name $id$,Glob_term.Explicit,$c1$,$c2$) >>
+        <:expr< Glob_term.GLambda ($dloc$,Name $id$,Decl_kinds.Explicit,$c1$,$c2$) >>
       | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
         <:expr< Glob_term.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
       (* fix todo *)
@@ -61,7 +62,7 @@ EXTEND
         <:expr< Glob_term.GCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
     | "90" RIGHTA
       [ c1 = constr; "->"; c2 = SELF ->
-        <:expr< Glob_term.GProd ($dloc$,Anonymous,Glob_term.Explicit,$c1$,$c2$) >> ]
+        <:expr< Glob_term.GProd ($dloc$,Anonymous,Decl_kinds.Explicit,$c1$,$c2$) >> ]
     | "75" RIGHTA
       [ "~"; c = constr ->
         apply_ref <:expr< coq_not_ref >> [c] ]
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index f36465207..6ef7ba1d8 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -51,18 +51,18 @@ let mlexpr_of_located f (loc,x) = <:expr< ($dloc$, $f x$) >>
 let mlexpr_of_loc loc = <:expr< $dloc$ >>
 
 let mlexpr_of_by_notation f = function
-  | Genarg.AN x -> <:expr< Genarg.AN $f x$ >>
-  | Genarg.ByNotation (loc,s,sco) ->
-      <:expr< Genarg.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
+  | Misctypes.AN x -> <:expr< Misctypes.AN $f x$ >>
+  | Misctypes.ByNotation (loc,s,sco) ->
+      <:expr< Misctypes.ByNotation $dloc$ $str:s$ $mlexpr_of_option mlexpr_of_string sco$ >>
 
 let mlexpr_of_intro_pattern = function
-  | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
-  | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
-  | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
-  | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
-  | Genarg.IntroIdentifier id ->
-      <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
-  | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ ->
+  | Misctypes.IntroWildcard -> <:expr< Misctypes.IntroWildcard >>
+  | Misctypes.IntroAnonymous -> <:expr< Misctypes.IntroAnonymous >>
+  | Misctypes.IntroFresh id -> <:expr< Misctypes.IntroFresh (mlexpr_of_ident $dloc$ id) >>
+  | Misctypes.IntroForthcoming b -> <:expr< Misctypes.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
+  | Misctypes.IntroIdentifier id ->
+      <:expr< Misctypes.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
+  | Misctypes.IntroOrAndPattern _ | Misctypes.IntroRewrite _ ->
       failwith "mlexpr_of_intro_pattern: TODO"
 
 let mlexpr_of_ident_option = mlexpr_of_option (mlexpr_of_ident)
@@ -72,34 +72,40 @@ let mlexpr_of_or_metaid f = function
   | Tacexpr.MetaId (_,id) -> <:expr< Tacexpr.AI $anti loc id$ >>
 
 let mlexpr_of_quantified_hypothesis = function
-  | Glob_term.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
-  | Glob_term.NamedHyp id ->  <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
+  | Misctypes.AnonHyp n -> <:expr< Glob_term.AnonHyp $mlexpr_of_int n$ >>
+  | Misctypes.NamedHyp id ->  <:expr< Glob_term.NamedHyp $mlexpr_of_ident id$ >>
 
 let mlexpr_of_or_var f = function
-  | Glob_term.ArgArg x -> <:expr< Glob_term.ArgArg $f x$ >>
-  | Glob_term.ArgVar id -> <:expr< Glob_term.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
+  | Misctypes.ArgArg x -> <:expr< Misctypes.ArgArg $f x$ >>
+  | Misctypes.ArgVar id -> <:expr< Misctypes.ArgVar $mlexpr_of_located mlexpr_of_ident id$ >>
 
 let mlexpr_of_hyp = mlexpr_of_or_metaid (mlexpr_of_located mlexpr_of_ident)
 
-let mlexpr_of_occs =
-  mlexpr_of_pair
-    mlexpr_of_bool (mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int))
+let mlexpr_of_occs = function
+  | Locus.AllOccurrences -> <:expr< Locus.AllOccurrences >>
+  | Locus.AllOccurrencesBut l ->
+    <:expr< Locus.AllOccurrencesBut
+      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
+  | Locus.NoOccurrences -> <:expr< Locus.NoOccurrences >>
+  | Locus.OnlyOccurrences l ->
+    <:expr< Locus.OnlyOccurrences
+      $mlexpr_of_list (mlexpr_of_or_var mlexpr_of_int) l$ >>
 
 let mlexpr_of_occurrences f = mlexpr_of_pair mlexpr_of_occs f
 
 let mlexpr_of_hyp_location = function
-  | occs, Termops.InHyp ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHyp) >>
-  | occs, Termops.InHypTypeOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypTypeOnly) >>
-  | occs, Termops.InHypValueOnly ->
-      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Termops.InHypValueOnly) >>
+  | occs, Locus.InHyp ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHyp) >>
+  | occs, Locus.InHypTypeOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypTypeOnly) >>
+  | occs, Locus.InHypValueOnly ->
+      <:expr< ($mlexpr_of_occurrences mlexpr_of_hyp occs$, Locus.InHypValueOnly) >>
 
 let mlexpr_of_clause cl =
-  <:expr< {Tacexpr.onhyps=
+  <:expr< {Locus.onhyps=
              $mlexpr_of_option (mlexpr_of_list mlexpr_of_hyp_location)
-               cl.Tacexpr.onhyps$;
-           Tacexpr.concl_occs= $mlexpr_of_occs cl.Tacexpr.concl_occs$} >>
+               cl.Locus.onhyps$;
+           Locus.concl_occs= $mlexpr_of_occs cl.Locus.concl_occs$} >>
 
 let mlexpr_of_red_flags {
   Glob_term.rBeta = bb;
@@ -120,8 +126,8 @@ let mlexpr_of_explicitation = function
   | Topconstr.ExplByPos (n,_id) -> <:expr< Topconstr.ExplByPos $mlexpr_of_int n$ >>
 
 let mlexpr_of_binding_kind = function
-  | Glob_term.Implicit -> <:expr< Glob_term.Implicit >>
-  | Glob_term.Explicit -> <:expr< Glob_term.Explicit >>
+  | Decl_kinds.Implicit -> <:expr< Decl_kinds.Implicit >>
+  | Decl_kinds.Explicit -> <:expr< Decl_kinds.Explicit >>
 
 let mlexpr_of_binder_kind = function
   | Topconstr.Default b -> <:expr< Topconstr.Default $mlexpr_of_binding_kind b$ >>
@@ -215,14 +221,14 @@ let rec mlexpr_of_may_eval f = function
       <:expr< Glob_term.ConstrTerm $mlexpr_of_constr c$ >>
 
 let mlexpr_of_binding_kind = function
-  | Glob_term.ExplicitBindings l ->
+  | Misctypes.ExplicitBindings l ->
       let l = mlexpr_of_list (mlexpr_of_triple mlexpr_of_loc mlexpr_of_quantified_hypothesis mlexpr_of_constr) l in
-      <:expr< Glob_term.ExplicitBindings $l$ >>
-  | Glob_term.ImplicitBindings l ->
+      <:expr< Misctypes.ExplicitBindings $l$ >>
+  | Misctypes.ImplicitBindings l ->
       let l = mlexpr_of_list mlexpr_of_constr l in
-      <:expr< Glob_term.ImplicitBindings $l$ >>
-  | Glob_term.NoBindings ->
-       <:expr< Glob_term.NoBindings >>
+      <:expr< Misctypes.ImplicitBindings $l$ >>
+  | Misctypes.NoBindings ->
+       <:expr< Misctypes.NoBindings >>
 
 let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr