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

 Corresponding operations in locusops.ml and miscops.ml

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

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

6 files changed, 28 insertions, 22 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 0357fc8a3c..8633658003 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -29,6 +29,7 @@ open Inductiveops
 open Tactics
 open Tacticals
 open Ind_tables
+open Misctypes
 
 (**********************************************************************)
 (* Generic synthesis of boolean equality *)
@@ -80,21 +81,21 @@ let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
 
 let induct_on c =
   new_induct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 let destruct_on_using c id =
   new_destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None
-    (None,Some (dl,Genarg.IntroOrAndPattern [
-                                    [dl,Genarg.IntroAnonymous];
-                                    [dl,Genarg.IntroIdentifier id]]))
+    (None,Some (dl,IntroOrAndPattern [
+                                    [dl,IntroAnonymous];
+                                    [dl,IntroIdentifier id]]))
     None
 
 let destruct_on c =
   new_destruct false
-    [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+    [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
     None (None,None) None
 
 (* reconstruct the inductive with the correct deBruijn indexes *)
@@ -537,7 +538,7 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
                      tclTRY (
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     simpl_in_hyp (freshz,InHyp);
+                     simpl_in_hyp (freshz,Locus.InHyp);
 (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
 *)
@@ -549,11 +550,11 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                            in
                             avoid := fresht::(!avoid);
                             (new_destruct false [Tacexpr.ElimOnConstr
-                                      (Evd.empty,((mkVar freshz,Glob_term.NoBindings)))]
+                                      (Evd.empty,((mkVar freshz,NoBindings)))]
                                   None
-                                  (None, Some (dl,Genarg.IntroOrAndPattern [[
-                                    dl,Genarg.IntroIdentifier fresht;
-                                    dl,Genarg.IntroIdentifier freshz]])) None) gl
+                                  (None, Some (dl,IntroOrAndPattern [[
+                                    dl,IntroIdentifier fresht;
+                                    dl,IntroIdentifier freshz]])) None) gl
                         ]);
 (*
   Ci a1 ... an = Ci b1 ... bn
@@ -667,7 +668,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
                      tclTRY (
                       tclORELSE reflexivity (Equality.discr_tac false None)
                      );
-                     Equality.inj [] false (mkVar freshz,Glob_term.NoBindings);
+                     Equality.inj [] false (mkVar freshz,NoBindings);
 		     intros; simpl_in_concl;
                      Auto.default_auto;
                      tclREPEAT (
@@ -837,10 +838,10 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
                   Auto.default_auto
 		]);
 	      Equality.general_rewrite_bindings_in true
-	                      all_occurrences true false
+	                      Locus.AllOccurrences true false
                               (List.hd !avoid)
                               ((mkVar (List.hd (List.tl !avoid))),
-                                Glob_term.NoBindings
+                                NoBindings
                               )
                               true;
               Equality.discr_tac false None
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9e21a3a761..ecc4e69953 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -31,6 +31,7 @@ open Evarutil
 open Evarconv
 open Notation
 open Indschemes
+open Misctypes
 
 let rec under_binders env f n c =
   if n = 0 then f env Evd.empty c else
@@ -351,7 +352,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun ((_,indname),_,ar,lc) -> {
     ind_name = indname;
-    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc, Glob_term.GType None)) ar;
+    ind_arity = Option.cata (fun x -> x) (CSort (dummy_loc,GType None)) ar;
     ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
   }) indl
 
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 21e39e0ca4..5a4dbabb6d 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -15,6 +15,7 @@ open Glob_term
 open Genarg
 open Vernacexpr
 open Ind_tables
+open Misctypes
 
 (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index fc51e13486..6ac321e43d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -34,6 +34,7 @@ open Redexpr
 open Syntax_def
 open Lemmas
 open Declaremods
+open Misctypes
 
 (* Pcoq hooks *)
 
@@ -42,7 +43,7 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : reference Genarg.or_by_notation -> unit;
+  print_name : reference or_by_notation -> unit;
   print_check : Environ.env -> Environ.unsafe_judgment -> unit;
   print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
     Environ.unsafe_judgment -> unit;
@@ -1319,8 +1320,8 @@ let vernac_search s r =
       Search.search_about (List.map (on_snd interp_search_about_item) sl) r
 
 let vernac_locate = function
-  | LocateTerm (Genarg.AN qid) -> msgnl (print_located_qualid qid)
-  | LocateTerm (Genarg.ByNotation (_,ntn,sc)) ->
+  | LocateTerm (AN qid) -> msgnl (print_located_qualid qid)
+  | LocateTerm (ByNotation (_,ntn,sc)) ->
       ppnl
         (Notation.locate_notation
           (Constrextern.without_symbols pr_lglob_constr) ntn sc)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index a9d384ea03..704f06fb51 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -11,6 +11,7 @@ open Term
 open Vernacinterp
 open Vernacexpr
 open Topconstr
+open Misctypes
 
 (** Vernacular entries *)
 
@@ -28,7 +29,7 @@ type pcoq_hook = {
   solve : int -> unit;
   abort : string -> unit;
   search : searchable -> dir_path list * bool -> unit;
-  print_name : Libnames.reference Genarg.or_by_notation -> unit;
+  print_name : Libnames.reference or_by_notation -> unit;
   print_check : Environ.env -> Environ.unsafe_judgment -> unit;
   print_eval : Reductionops.reduction_function -> Environ.env -> Evd.evar_map -> constr_expr ->
     Environ.unsafe_judgment -> unit;
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 1882e0af24..5ccf8db88b 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -26,6 +26,7 @@ open Pfedit
 open Refiner
 open Tacmach
 open Syntax_def
+open Misctypes
 
 (* Coq interface to the Whelp query engine developed at
    the University of Bologna *)
@@ -94,8 +95,8 @@ let url_paren f l = url_char '('; f l; url_char ')'
 let url_bracket f l = url_char '['; f l; url_char ']'
 
 let whelp_of_glob_sort = function
-  | GProp Null -> "Prop"
-  | GProp Pos -> "Set"
+  | GProp -> "Prop"
+  | GSet -> "Set"
   | GType _ -> "Type"
 
 let uri_int n = Buffer.add_string b (string_of_int n)
@@ -163,7 +164,7 @@ let rec uri_of_constr c =
   | GLetIn (_,na,b,c) ->
       url_string "let "; url_of_name na; url_string "\\def ";
       uri_of_constr b; url_string " in "; uri_of_constr c
-  | GCast (_,c, CastConv (_,t)) ->
+  | GCast (_,c, (CastConv t|CastVM t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
   | GRec _ | GIf _ | GLetTuple _ | GCases _ ->
       error "Whelp does not support pattern-matching and (co-)fixpoint."