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

2 files changed, 10 insertions, 8 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index a1e968668a..58111f597e 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -19,6 +19,8 @@ open Glob_term
 open Term
 open Pp
 open Compat
+open Decl_kinds
+open Misctypes
 
 (* INTERN *)
 
@@ -194,7 +196,7 @@ let abstract_one_hyp inject h glob =
 let glob_constr_of_hyps inject hyps head =
   List.fold_right (abstract_one_hyp inject) hyps head
 
-let glob_prop = GSort (dummy_loc,GProp Null)
+let glob_prop = GSort (dummy_loc,GProp)
 
 let rec match_hyps blend names constr = function
     [] -> [],substl names constr
@@ -345,13 +347,13 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
       glob_app(dummy_loc,rind,rparams@rparams_rec@dum_args) in
   let pat_vars,aliases,patt = interp_pattern env pat in
   let inject = function
-      Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp Null)
+      Thesis (Plain) -> Glob_term.GSort(dummy_loc,GProp)
     | Thesis (For rec_occ) ->
 	if not (List.mem rec_occ pat_vars) then
 	  errorlabstrm "suppose it is"
 	    (str "Variable " ++ Nameops.pr_id rec_occ ++
 	       str " does not occur in pattern.");
-	Glob_term.GSort(dummy_loc,GProp Null)
+	Glob_term.GSort(dummy_loc,GProp)
     | This (c,_) -> c in
   let term1 = glob_constr_of_hyps inject hyps glob_prop in
   let loc_ids,npatt =
@@ -361,7 +363,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let term2 =
     GLetIn(dummy_loc,Anonymous,
 	   GCast(dummy_loc,glob_of_pat npatt,
-		 CastConv (DEFAULTcast,app_ind)),term1) in
+		 CastConv app_ind),term1) in
   let term3=List.fold_right let_in_one_alias aliases term2 in
   let term4=List.fold_right prod_one_id loc_ids term3 in
   let term5=List.fold_right prod_one_hyp params term4 in
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 2870e8f7e1..956a561aa6 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -29,7 +29,7 @@ open Termops
 open Namegen
 open Reductionops
 open Goptions
-
+open Misctypes
 
 (* Strictness option *)
 
@@ -237,7 +237,7 @@ let add_justification_hyps keep items gls =
       | _ ->
 	  let id=pf_get_new_id local_hyp_prefix gls in
 	    keep:=Idset.add id !keep;
-	    tclTHEN (letin_tac None (Names.Name id) c None Tacexpr.nowhere)
+	    tclTHEN (letin_tac None (Names.Name id) c None Locusops.nowhere)
               (thin_body [id]) gls in
     tclMAP add_aux items gls
 
@@ -750,7 +750,7 @@ let consider_tac c hyps gls =
     | _ ->
 	let id = pf_get_new_id (id_of_string "_tmp") gls in
 	tclTHEN
-	  (forward None (Some (dummy_loc, Genarg.IntroIdentifier id)) c)
+	  (forward None (Some (dummy_loc, IntroIdentifier id)) c)
  	  (consider_match false [] [id] hyps) gls
 
 
@@ -781,7 +781,7 @@ let rec build_function args body =
 
 let define_tac id args body gls =
   let t = build_function args body in
-    letin_tac None (Name id) t None Tacexpr.nowhere gls
+    letin_tac None (Name id) t None Locusops.nowhere gls
 
 (* tactics for reconsider *)