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

12 files changed, 105 insertions, 97 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 4d5cbe223..5bf772fc5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -15,6 +15,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Libnames
+open Misctypes
 
 let msgnl = Pp.msgnl
 
@@ -441,13 +442,8 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	 decompose_prod_n_assum (List.length context) reduced_type_of_hyp
       in
         tclTHENLIST
-	[
-	  h_reduce_with_zeta
-	    (Tacticals.onHyp hyp_id)
-	  ;
-	  scan_type new_context new_typ_of_hyp
-
-	]
+	[ h_reduce_with_zeta (Locusops.onHyp hyp_id);
+	  scan_type new_context new_typ_of_hyp ]
     else if isProd type_of_hyp
     then
       begin
@@ -688,13 +684,13 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
   if args_id = []
   then
     tclTHENLIST [
-      tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+      tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
       do_prove hyps
     ]
   else
     tclTHENLIST
       [
-	tclMAP (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id)) hyps;
+	tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
 	tclMAP instanciate_one_hyp hyps;
 	(fun g ->
 	   let all_g_hyps_id =
@@ -732,7 +728,7 @@ let build_proof
 		    [
 		      h_generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
 		      thin dyn_infos.rec_hyps;
-		      pattern_option [(false,[1]),t] None;
+		      pattern_option [Locus.AllOccurrencesBut [1],t] None;
 		      (fun g -> observe_tac "toto" (
 			 tclTHENSEQ [h_simplest_case t;
 				     (fun g' ->
@@ -818,9 +814,10 @@ let build_proof
 
 		      tclTHENLIST
 			[tclMAP
-			   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
+			   (fun hyp_id ->
+			     h_reduce_with_zeta (Locusops.onHyp hyp_id))
 			   dyn_infos.rec_hyps;
-			 h_reduce_with_zeta Tacticals.onConcl;
+			 h_reduce_with_zeta Locusops.onConcl;
 			 build_proof do_finalize new_infos
 			]
 			g
@@ -850,9 +847,9 @@ let build_proof
 
 	      tclTHENLIST
 		[tclMAP
-		   (fun hyp_id -> h_reduce_with_zeta (Tacticals.onHyp hyp_id))
+		   (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id))
 		   dyn_infos.rec_hyps;
-		 h_reduce_with_zeta Tacticals.onConcl;
+		 h_reduce_with_zeta Locusops.onConcl;
 		 build_proof do_finalize new_infos
 		] g
 	  | Rel _ -> anomaly "Free var in goal conclusion !"
@@ -1010,7 +1007,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	   let rec_id = pf_nth_hyp_id g 1 in
 	   tclTHENSEQ
 	     [(* observe_tac "generalize_non_dep in generate_equation_lemma" *) (generalize_non_dep rec_id);
-	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,Glob_term.NoBindings));
+	      (* observe_tac "h_case" *) (h_case false (mkVar rec_id,NoBindings));
 	      intros_reflexivity] g
 	)
       ]
@@ -1346,7 +1343,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		 in
 		 let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
 		 tclTHENSEQ
-		   [unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef fname)];
+		   [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef fname)];
 		    let do_prove =
 		      build_proof
 			interactive_proof
@@ -1442,12 +1439,12 @@ let backtrack_eqs_until_hrec hrec eqs : tactic =
 
 let build_clause eqs =
   {
-    Tacexpr.onhyps =
+    Locus.onhyps =
       Some (List.map
-	      (fun id -> (Glob_term.all_occurrences_expr, id), Termops.InHyp)
+	      (fun id -> (Locus.AllOccurrences, id), Locus.InHyp)
 	      eqs
 	   );
-    Tacexpr.concl_occs = Glob_term.no_occurrences_expr
+    Locus.concl_occs = Locus.NoOccurrences
   }
 
 let rec rewrite_eqs_in_eqs eqs =
@@ -1460,7 +1457,8 @@ let rec rewrite_eqs_in_eqs eqs =
 	       (fun id gl ->
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
-		    (tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* dep proofs also: *) true id (mkVar eq) false))
+		    (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences
+			       true (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
 	       )
 	       eqs
@@ -1482,7 +1480,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 		  (fun g ->
 		     if is_mes
 		     then
-		       unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+		       unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
 		     else tclIDTAC g
 		  );
 		  observe_tac "rew_and_finish"
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 0f776ee6e..b38503cb9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -15,6 +15,7 @@ open Tacticals
 open Tactics
 open Indfun_common
 open Functional_principles_proofs
+open Misctypes
 
 exception Toberemoved_with_rel of int*constr
 exception Toberemoved
@@ -504,7 +505,7 @@ let get_funs_constant mp dp =
 exception No_graph_found
 exception Found_type of int
 
-let make_scheme (fas : (constant*Glob_term.glob_sort) list) : Entries.definition_entry list =
+let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry list =
   let env = Global.env ()
   and sigma = Evd.empty in
   let funs = List.map fst fas in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 1c02c16ec..00d130d28 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,6 +1,6 @@
 open Names
 open Term
-
+open Misctypes
 
 val generate_functional_principle :
   (* do we accept interactive proving *)
@@ -27,8 +27,8 @@ val compute_new_princ_type_from_rel : constr array -> sorts array ->
 
 exception No_graph_found
 
-val make_scheme : (constant*Glob_term.glob_sort) list -> Entries.definition_entry list
+val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list
 
-val build_scheme : (identifier*Libnames.reference*Glob_term.glob_sort) list ->  unit
-val build_case_scheme : (identifier*Libnames.reference*Glob_term.glob_sort)  ->  unit
+val build_scheme : (identifier*Libnames.reference*glob_sort) list ->  unit
+val build_case_scheme : (identifier*Libnames.reference*glob_sort)  ->  unit
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e8fec0dd8..aed71c3ae 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -17,19 +17,20 @@ open Genarg
 open Pcoq
 open Tacticals
 open Constr
+open Misctypes
 
 let pr_binding prc = function
-  | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
-  | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+  | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
+  | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
 
 let pr_bindings prc prlc = function
-  | Glob_term.ImplicitBindings l ->
+  | ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
       pr_sequence prc l
-  | Glob_term.ExplicitBindings l ->
+  | ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
         pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | Glob_term.NoBindings -> mt ()
+  | NoBindings -> mt ()
 
 let pr_with_bindings prc prlc (c,bl) =
   prc c ++ hv 0 (pr_bindings prc prlc bl)
@@ -308,7 +309,7 @@ let mkEq typ c1 c2 =
 let poseq_unsafe idunsafe cstr gl =
   let typ = Tacmach.pf_type_of gl cstr in
   tclTHEN
-    (Tactics.letin_tac None (Name idunsafe) cstr None allHypsAndConcl)
+    (Tactics.letin_tac None (Name idunsafe) cstr None Locusops.allHypsAndConcl)
     (tclTHENFIRST
       (Tactics.assert_tac Anonymous (mkEq typ (mkVar idunsafe) cstr))
       Tactics.reflexivity)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 954e389a4..f18309d04 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -8,6 +8,7 @@ open Indfun_common
 open Errors
 open Util
 open Glob_termops
+open Misctypes
 
 let observe strm =
   if do_observe ()
@@ -1258,7 +1259,8 @@ let rec rebuild_return_type rt =
 	Topconstr.CProdN(loc,n,rebuild_return_type t')
     | Topconstr.CLetIn(loc,na,t,t') ->
 	Topconstr.CLetIn(loc,na,t,rebuild_return_type t')
-    | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],Topconstr.Default Glob_term.Explicit,rt],
+    | _ -> Topconstr.CProdN(dummy_loc,[[dummy_loc,Names.Anonymous],
+				       Topconstr.Default Decl_kinds.Explicit,rt],
 			    Topconstr.CSort(dummy_loc,GType None))
 
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index b14197891..6433fe37c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -3,6 +3,9 @@ open Glob_term
 open Errors
 open Util
 open Names
+open Decl_kinds
+open Misctypes
+
 (* Ocaml 3.06 Map.S does not handle is_empty *)
 let idmap_is_empty m = m = Idmap.empty
 
@@ -19,7 +22,7 @@ let mkGLetIn(n,t,b) = GLetIn(dummy_loc,n,t,b)
 let mkGCases(rto,l,brl) = GCases(dummy_loc,Term.RegularStyle,rto,l,brl)
 let mkGSort s = GSort(dummy_loc,s)
 let mkGHole () = GHole(dummy_loc,Evar_kinds.BinderType Anonymous)
-let mkGCast(b,t) = GCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t))
+let mkGCast(b,t) = GCast(dummy_loc,b,CastConv t)
 
 (*
   Some basic functions to decompose glob_constrs
@@ -180,10 +183,9 @@ let change_vars =
       | GRec _ -> error "Local (co)fixes are not supported"
       | GSort _ -> rt
       | GHole _ -> rt
-      | GCast(loc,b,CastConv (k,t)) ->
-	  GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
-      | GCast(loc,b,CastCoerce) ->
-	  GCast(loc,change_vars mapping b,CastCoerce)
+      | GCast(loc,b,c) ->
+	  GCast(loc,change_vars mapping b,
+		Miscops.map_cast_type (change_vars mapping) c)
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
     let new_mapping = List.fold_right Idmap.remove idl mapping in
     if idmap_is_empty new_mapping
@@ -360,10 +362,9 @@ let rec alpha_rt excluded rt =
     | GRec _ -> error "Not handled GRec"
     | GSort _ -> rt
     | GHole _ -> rt
-    | GCast (loc,b,CastConv (k,t)) ->
-	GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
-    | GCast (loc,b,CastCoerce) ->
-	GCast(loc,alpha_rt excluded b,CastCoerce)
+    | GCast (loc,b,c) ->
+	GCast(loc,alpha_rt excluded b,
+	      Miscops.map_cast_type (alpha_rt excluded) c)
     | GApp(loc,f,args) ->
 	GApp(loc,
 	     alpha_rt excluded f,
@@ -411,7 +412,7 @@ let is_free_in id =
     | GRec _ -> raise (UserError("",str "Not handled GRec"))
     | GSort _ -> false
     | GHole _ -> false
-    | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
+    | GCast (_,b,(CastConv t|CastVM t)) -> is_free_in b || is_free_in t
     | GCast (_,b,CastCoerce) -> is_free_in b
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
@@ -507,10 +508,9 @@ let replace_var_by_term x_id term =
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
-      | GCast(loc,b,CastConv(k,t)) ->
-	  GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
-      | GCast(loc,b,CastCoerce) ->
-	  GCast(loc,replace_var_by_pattern b,CastCoerce)
+      | GCast(loc,b,c) ->
+	  GCast(loc,replace_var_by_pattern b,
+		Miscops.map_cast_type replace_var_by_pattern c)
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
     if List.exists (fun id -> id_ord id x_id == 0) idl
     then br
@@ -593,7 +593,7 @@ let ids_of_glob_constr c =
       | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
       | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc
       | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc
-      | GCast (loc,c,CastConv(k,t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
+      | GCast (loc,c,(CastConv t|CastVM t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc
       | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc
       | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc
       | GLetTuple (_,nal,(na,po),b,c) ->
@@ -661,10 +661,9 @@ let zeta_normalize =
       | GRec _ -> raise (UserError("",str "Not handled GRec"))
       | GSort _ -> rt
       | GHole _ -> rt
-      | GCast(loc,b,CastConv(k,t)) ->
-	  GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
-      | GCast(loc,b,CastCoerce) ->
-	  GCast(loc,zeta_normalize_term b,CastCoerce)
+      | GCast(loc,b,c) ->
+	  GCast(loc,zeta_normalize_term b,
+                Miscops.map_cast_type zeta_normalize_term c)
   and zeta_normalize_br (loc,idl,patl,res) =
     (loc,idl,patl,zeta_normalize_term res)
   in
@@ -702,8 +701,9 @@ let expand_as =
 	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
-      | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t))
-      | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce)
+      | GCast(loc,b,c) ->
+	  GCast(loc,expand_as map b,
+		Miscops.map_cast_type (expand_as map) c)
       | GCases(loc,sty,po,el,brl) ->
 	  GCases(loc, sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
 		List.map (expand_as_br map) brl)
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 80a8811f1..761337b07 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,4 +1,5 @@
 open Glob_term
+open Misctypes
 
 (* Ocaml 3.06 Map.S does not handle is_empty *)
 val idmap_is_empty : 'a Names.Idmap.t -> bool
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 42df294a0..96bde6f1b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -7,6 +7,8 @@ open Indfun_common
 open Libnames
 open Glob_term
 open Declarations
+open Misctypes
+open Decl_kinds
 
 let is_rec_info scheme_info =
   let test_branche min acc (_,_,br) =
@@ -64,7 +66,7 @@ let functional_induction with_clean c princl pat =
 			  errorlabstrm "" (str "Cannot find induction principle for "
 					   ++Printer.pr_lconstr (mkConst c') )
 		    in
-		    (princ,Glob_term.NoBindings, Tacmach.pf_type_of g princ)
+		    (princ,NoBindings, Tacmach.pf_type_of g princ)
 		| _ -> raise (UserError("",str "functional induction must be used with a function" ))
 	    end
 	| Some ((princ,binding)) ->
@@ -109,7 +111,7 @@ let functional_induction with_clean c princl pat =
 	in
 	Tacticals.tclTHEN
 	  (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl )
-	  (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl)
+	  (Hiddentac.h_reduce flag Locusops.allHypsAndConcl)
 	  g
       else Tacticals.tclIDTAC g
     in
@@ -480,7 +482,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	    let b = Names.id_of_string "___b" in 
 	    Topconstr.mkLambdaC(
 	      [dummy_loc,Name a;dummy_loc,Name b],
-	      Topconstr.Default Lib.Explicit,
+	      Topconstr.Default Explicit,
 	      wf_arg_type,
 	      Topconstr.mkAppC(wf_rel_expr,
 			       [
@@ -744,10 +746,9 @@ let rec add_args id new_args b =
   | CPatVar _ -> b
   | CEvar _ -> b
   | CSort _ -> b
-  | CCast(loc,b1,CastConv(ck,b2))  ->
-      CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2))
-  | CCast(loc,b1,CastCoerce) ->
-      CCast(loc,add_args id new_args b1,CastCoerce)
+  | CCast(loc,b1,b2)  ->
+      CCast(loc,add_args id new_args b1,
+	    Miscops.map_cast_type (add_args id new_args) b2)
   | CRecord (loc, w, pars) ->
       CRecord (loc,
 	       (match w with Some w -> Some (add_args id new_args w) | _ -> None),
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index faa5f2e46..c0b72f0b3 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -7,6 +7,7 @@ open Indfun_common
 open Libnames
 open Glob_term
 open Declarations
+open Misctypes
 
 val do_generate_principle :  
   bool -> 
@@ -17,8 +18,8 @@ val do_generate_principle :
 val functional_induction :  
   bool ->
   Term.constr ->
-  (Term.constr * Term.constr Glob_term.bindings) option ->
-  Genarg.intro_pattern_expr Pp.located option ->
+  (Term.constr * Term.constr bindings) option ->
+  intro_pattern_expr Pp.located option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b92a8daf3..667be89d0 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -19,22 +19,23 @@ open Indfun_common
 open Tacmach
 open Sign
 open Hiddentac
+open Misctypes
 
 (* Some pretty printing function for debugging purpose *)
 
 let pr_binding prc  =
   function
-    | loc, Glob_term.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
-    | loc, Glob_term.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c)
+    | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c)
 
 let pr_bindings prc prlc = function
-  | Glob_term.ImplicitBindings l ->
+  | ImplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
       pr_sequence prc l
-  | Glob_term.ExplicitBindings l ->
+  | ExplicitBindings l ->
       brk (1,1) ++ str "with" ++ brk (1,1) ++
         pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l
-  | Glob_term.NoBindings -> mt ()
+  | NoBindings -> mt ()
 
 
 let pr_with_bindings prc prlc (c,bl) =
@@ -272,7 +273,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> dummy_loc, Genarg.IntroIdentifier id)
+	     (fun id -> dummy_loc, IntroIdentifier id)
 	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
@@ -319,7 +320,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	       match b with
 		 | None -> pre_tac
 		 | Some b ->
-		   tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
+		   tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac
 	     else pre_tac
 	  )
 	  (pf_hyps g)
@@ -330,7 +331,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       	List.fold_right
       	  (fun (_,pat) acc ->
       	     match pat with
-      	       | Genarg.IntroIdentifier id -> id::acc
+	       | IntroIdentifier id -> id::acc
       	       | _ -> anomaly "Not an identifier"
       	  )
       	  (List.nth intro_pats (pred i))
@@ -420,7 +421,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 		     Glob_term.rConst = []
 		 }
 	      )
-	      onConcl;
+	      Locusops.onConcl;
 	    observe_tac ("toto ") tclIDTAC;
     
 	    (* introducing the the result of the graph and the equality hypothesis *)
@@ -571,7 +572,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 		 | None -> (id::pre_args,pre_tac)
 		 | Some b ->
 		     (pre_args,
-		      tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
+		      tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.AllOccurrences,EvalVarRef id])) allHyps) pre_tac
 		     )
 	     else (pre_args,pre_tac)
 	  )
@@ -754,15 +755,15 @@ and intros_with_rewrite_aux : tactic =
 			tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
-			unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))];
-			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Termops.InHyp) )) 
+			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
+			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
 		      else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) 
 		      then tclTHENSEQ[
-			unfold_in_concl [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))];
-			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Termops.all_occurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Termops.InHyp) )) 
+			unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))];
+			tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
@@ -797,7 +798,7 @@ and intros_with_rewrite_aux : tactic =
 		      Tauto.tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			h_case false (v,Glob_term.NoBindings);
+			h_case false (v,NoBindings);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -807,7 +808,7 @@ and intros_with_rewrite_aux : tactic =
 			     {Glob_term.all_flags
 			      with Glob_term.rDelta = false;
 			     })
-			  onConcl
+			  Locusops.onConcl
 			;
 			intros_with_rewrite
 		      ] g
@@ -822,7 +823,7 @@ and intros_with_rewrite_aux : tactic =
 		     {Glob_term.all_flags
 		      with Glob_term.rDelta = false;
 		     })
-		  onConcl
+		  Locusops.onConcl
 		;
 		intros_with_rewrite
 	      ] g
@@ -834,7 +835,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      h_case false (v,Glob_term.NoBindings);
+	      h_case false (v,NoBindings);
 	      intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -961,12 +962,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       {Glob_term.all_flags
 		with Glob_term.rDelta = false;
 	       })
-	    onConcl
+	    Locusops.onConcl
 	  ;
 	  h_generalize (List.map mkVar ids);
 	  thin ids
 	]
-      else unfold_in_concl [(Termops.all_occurrences, Names.EvalConstRef (destConst f))]
+      else unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (destConst f))]
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
@@ -1004,7 +1005,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(h_generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]);
 	h_intro graph_principle_id;
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" ((elim false (mkVar hres,Glob_term.NoBindings) (Some (mkVar graph_principle_id,Glob_term.NoBindings)))))
+	  (observe_tac "elim" ((elim false (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -1056,7 +1057,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	       (fun entry ->
 		  (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
 	       )
-	       (make_scheme (array_map_to_list (fun const -> const,Glob_term.GType None) funs))
+	       (make_scheme (array_map_to_list (fun const -> const,GType None) funs))
 	    )
     in
     let proving_tac =
@@ -1209,7 +1210,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
 	      | App(f,f_args),_ when eq_constr f fconst ->
-		  ((fun hid -> h_symmetry (onHyp hid)),f_args,args.(2))
+		  ((fun hid -> h_symmetry (Locusops.onHyp hid)),f_args,args.(2))
 	      |_,App(f,f_args) when eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
@@ -1219,7 +1220,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
 	    h_intro hid;
-	    Inv.inv FullInversion None (Glob_term.NamedHyp hid);
+	    Inv.inv FullInversion None (NamedHyp hid);
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3ea9c3d3e..0ec5f7bce 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -23,6 +23,7 @@ open Declarations
 open Environ
 open Glob_term
 open Glob_termops
+open Decl_kinds
 
 (** {1 Utilities}  *)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 8eb7d0e8f..d11909043 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -44,7 +44,7 @@ open Equality
 open Auto
 open Eauto
 
-open Genarg
+open Misctypes
 open Indfun_common
 
 
@@ -288,7 +288,7 @@ let tclUSER tac is_mes l g =
       if is_mes
       then tclTHENLIST
         [
-	  unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference
+	  unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
             (delayed_force Indfun_common.ltof_ref))];
          tac
 	 ]
@@ -566,9 +566,9 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
 		   tclTHENLIST[
 		     observe_tac (str "clearing k ") (clear [id]);
 		     h_intros [k;h';def];
-		     observe_tac (str "simple_iter") (simpl_iter onConcl);
+		     observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
 		     observe_tac (str "unfold functional")
-		       (unfold_in_concl[((true,[1]),
+		       (unfold_in_concl[(Locus.OnlyOccurrences [1],
 					 evaluable_of_global_reference infos.func)]);
 		     observe_tac (str "test" ) (
 		       tclTHENLIST[
@@ -685,7 +685,7 @@ let mkDestructEq :
      [h_generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
-	  (pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
+	  (pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2);
       simplest_case expr], to_revert
 
 
@@ -857,7 +857,7 @@ let rec make_rewrite_list expr_info max = function
 	    let def_na,_,_ = destProd t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
-	  general_rewrite_bindings false Termops.all_occurrences
+	  general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[dummy_loc,NamedHyp def,
@@ -883,7 +883,8 @@ let make_rewrite expr_info l hp max =
 	    let def_na,_,_ = destProd t in
 	    Nameops.out_name k_na,Nameops.out_name def_na
 	  in
-	 observe_tac (str "general_rewrite_bindings") (general_rewrite_bindings false Termops.all_occurrences
+	 observe_tac (str "general_rewrite_bindings")
+	   (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
 	     ExplicitBindings[dummy_loc,NamedHyp def,
@@ -892,9 +893,9 @@ let make_rewrite expr_info l hp max =
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (tclTHENLIST[
-	   simpl_iter onConcl;
+	   simpl_iter Locusops.onConcl;
 	   observe_tac (str "unfold functional")
-	     (unfold_in_concl[((true,[1]),
+	     (unfold_in_concl[(Locus.OnlyOccurrences [1],
 			       evaluable_of_global_reference expr_info.func)]);
 	   
 	   (list_rewrite true 
@@ -1413,7 +1414,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
   let x = n_x_id ids nargs in
   tclTHENLIST [
     h_intros x;
-    unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)];
+    unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
     observe_tac (str "simplest_case")
       (simplest_case (mkApp (terminate_constr,
                              Array.of_list (List.map mkVar x))));