Merge PR#718: API cleanup: aliases

13 files changed, 100 insertions, 100 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 023cbad43..ef894b239 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -106,7 +106,7 @@ let make_refl_eq constructor type_of_t t  =
 
 type pte_info =
     {
-      proving_tac : (Id.t list ->  Tacmach.tactic);
+      proving_tac : (Id.t list -> Proof_type.tactic);
       is_valid : constr -> bool
     }
 
@@ -688,7 +688,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
 
 let build_proof
     (interactive_proof:bool)
-    (fnames:constant list)
+    (fnames:Constant.t list)
     ptes_infos
     dyn_infos
     : tactic =
@@ -708,13 +708,13 @@ let build_proof
 		  let term_eq =
 		    make_refl_eq (Lazy.force refl_equal) type_of_term t
 		  in
-		  tclTHENSEQ
+		  tclTHENLIST
 		    [
 		      Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps)));
 		      thin dyn_infos.rec_hyps;
 		      Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
 		      (fun g -> observe_tac "toto" (
-			 tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
+			 tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
 				     (fun g' ->
 					let g'_nb_prod = nb_prod (project g') (pf_concl g') in
 					let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
@@ -982,14 +982,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
   (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *)
-  let f_id = Label.to_id (con_label (fst (destConst evd f))) in
+  let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in
   let prove_replacement =
-    tclTHENSEQ
+    tclTHENLIST
       [
 	tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro);
 	observe_tac "" (fun g ->
 	   let rec_id = pf_nth_hyp_id g 1 in
-	   tclTHENSEQ
+	   tclTHENLIST
 	     [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id);
 	      observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id)));
 	      (Proofview.V82.of_tactic intros_reflexivity)] g
@@ -1019,7 +1019,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
-      let f_id = Label.to_id (con_label (fst (destConst !evd f))) in
+      let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
 	i*)
@@ -1242,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		other_fix_infos 0)
     in
     let first_tac : tactic = (* every operations until fix creations *)
-      tclTHENSEQ
+      tclTHENLIST
 	[ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params)));
 	  observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates)));
 	  observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches)));
@@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
           in
 	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 	      (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro));
 	      (fun g -> (* replacement of the function by its body *)
@@ -1279,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     eq_hyps = []
 		   }
 		 in
-		 tclTHENSEQ
+		 tclTHENLIST
 		   [
 		     observe_tac "do_replace"
 		       (do_replace evd
@@ -1322,7 +1322,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	    ] gl
 	with Not_found ->
 	  let nb_args = min (princ_info.nargs) (List.length ctxt) in
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 	      tclDO nb_args (Proofview.V82.of_tactic intro);
 	      (fun g -> (* replacement of the function by its body *)
@@ -1343,7 +1343,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   }
 		 in
 		 let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in
-		 tclTHENSEQ
+		 tclTHENLIST
 		   [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
 		    let do_prove =
 		      build_proof
@@ -1402,7 +1402,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 	fun gls ->
 (* 	  let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
 (* 	  let ids = hid::pf_ids_of_hyps gls in  *)
-	  tclTHENSEQ
+	  tclTHENLIST
 	    [
 (* 	      generalize [lemma]; *)
 (* 	      h_intro hid; *)
@@ -1457,13 +1457,13 @@ let rec rewrite_eqs_in_eqs eqs =
 
 let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
   fun gls ->
-    (tclTHENSEQ
+    (tclTHENLIST
        [
 	 backtrack_eqs_until_hrec hrec eqs;
 	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
 	    (Proofview.V82.of_tactic (apply (mkVar hrec)))
-	    [ tclTHENSEQ
+	    [ tclTHENLIST
 		[
 		  (Proofview.V82.of_tactic (keep (tcc_hyps@eqs)));
 		  (Proofview.V82.of_tactic (apply (Lazy.force acc_inv)));
@@ -1617,7 +1617,7 @@ let prove_principle_for_gen
 	  (Id.of_string "prov")
 	  hyps
       in
-      tclTHENSEQ
+      tclTHENLIST
 	[
 	  Proofview.V82.of_tactic (generalize [lemma]);
 	  Proofview.V82.of_tactic (Simple.intro hid);
@@ -1636,7 +1636,7 @@ let prove_principle_for_gen
 	  ]
 	  gls
   in
-  tclTHENSEQ
+  tclTHENLIST
     [
       observe_tac "start_tac" start_tac;
       h_intros
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 069f767dd..5bb288678 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -4,17 +4,17 @@ open Names
 val prove_princ_for_struct :
   Evd.evar_map ref ->
   bool ->
-  int -> constant array -> EConstr.constr array -> int -> Tacmach.tactic
+  int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic
 
 
 val prove_principle_for_gen :
-  constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
+  Constant.t * Constant.t * Constant.t -> (* name of the function, the functional and the fixpoint equation *)
   Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
   bool -> (* is that function uses measure *)
   int -> (* the number of recursive argument *)
   EConstr.types -> (* the type of the recursive argument *)
   EConstr.constr -> (* the wf relation used to prove the function *)
-  Tacmach.tactic
+  Proof_type.tactic
 
 
 (* val is_pte  : rel_declaration -> bool  *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index fd4b52b65..70245a8b1 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -150,7 +150,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
 		([],[])
 	    in
 	    let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in
-	    applist(new_f, new_args),
+	    applistc new_f new_args,
 	    list_union_eq eq_constr binders_to_remove_from_f binders_to_remove
 	| LetIn(x,v,t,b) ->
 	    compute_new_princ_type_for_letin remove env x v t b
@@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
     match new_princ_name with
       | Some (id) -> id,id
       | None ->
-	  let id_of_f = Label.to_id (con_label (fst f)) in
+	  let id_of_f = Label.to_id (Constant.label (fst f)) in
 	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let names = ref [new_princ_name] in
@@ -389,14 +389,14 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 exception Not_Rec
 
 let get_funs_constant mp dp =
-  let get_funs_constant const e : (Names.constant*int) array =
+  let get_funs_constant const e : (Names.Constant.t*int) array =
     match kind_of_term ((strip_lam e)) with
       | Fix((_,(na,_,_))) ->
 	  Array.mapi
 	    (fun i na ->
 	       match na with
 		 | Name id ->
-		     let const = make_con mp dp (Label.of_id id) in
+		     let const = Constant.make3 mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
 		     anomaly (Pp.str "Anonymous fix.")
@@ -656,7 +656,7 @@ let build_case_scheme fa =
       user_err ~hdr:"FunInd.build_case_scheme"
         (str "Cannot find " ++ Libnames.pr_reference f) in
   let first_fun,u = destConst  funs in
-  let funs_mp,funs_dp,_ = Names.repr_con first_fun in
+  let funs_mp,funs_dp,_ = Constant.repr3 first_fun in
   let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
   let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in
   let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index bf1906bfb..bb2b2d918 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -18,7 +18,7 @@ val generate_functional_principle :
   (* induction principle on rel *)
   types ->
   (* *)
-  sorts array option ->
+  Sorts.t array option ->
   (* Name of the new principle *)
   (Id.t) option ->
   (* the compute functions to use   *)
@@ -28,10 +28,10 @@ val generate_functional_principle :
   (* The tactic to use to make the proof w.r
      the number of params
   *)
-  (EConstr.constr array -> int -> Tacmach.tactic) ->
+  (EConstr.constr array -> int -> Proof_type.tactic) ->
   unit
 
-val compute_new_princ_type_from_rel : constr array -> sorts array ->
+val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
   types -> types
 
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d9cd026d8..1258c9286 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
 END
 
 let pr_fun_scheme_arg (princ_name,fun_name,s) =
-  Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
+  Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
   Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++
   Ppconstr.pr_glob_sort s
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index eae72d9e8..a7481370a 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -579,8 +579,8 @@ let ids_of_pat =
   ids_of_pat Id.Set.empty
 
 let id_of_name = function
-  | Names.Anonymous -> Id.of_string "x"
-  | Names.Name x -> x
+  | Anonymous -> Id.of_string "x"
+  | Name x -> x
 
 (* TODO: finish Rec caes *)
 let ids_of_glob_constr c =
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f277c563a..d12aa7f42 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -65,7 +65,7 @@ let functional_induction with_clean c princl pat =
 			  (or f_rec, f_rect) i*)
 		  let princ_name =
 		    Indrec.make_elimination_ident
-		      (Label.to_id (con_label c'))
+		      (Label.to_id (Constant.label c'))
 		      (Tacticals.elimination_sort_of_goal g)
 		  in
 		  try
@@ -342,8 +342,8 @@ let error_error names e =
 
 let generate_principle (evd:Evd.evar_map ref) pconstants on_error
     is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs  interactive_proof
-    (continue_proof : int -> Names.constant array -> EConstr.constr array -> int ->
-      Tacmach.tactic) : unit =
+    (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
+      Proof_type.tactic) : unit =
   let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
   let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
   let funs_args = List.map fst fun_bodies in
@@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
-    (_: int) (_:Names.constant array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
+    (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic =
   Functional_principles_proofs.prove_principle_for_gen
     (f_ref,functional_ref,eq_ref)
     tcc_lemma_ref is_mes  rec_arg_num rec_arg_type relation
@@ -899,14 +899,14 @@ let make_graph (f_ref:global_reference) =
 		 in
 		 l
 	     | _ ->
-		let id = Label.to_id (con_label c) in
+		let id = Label.to_id (Constant.label c) in
 		 [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
-	 let mp,dp,_ = repr_con c in
+	 let mp,dp,_ = Constant.repr3 c in
 	 do_generate_principle [c,Univ.Instance.empty] error_error  false false expr_list;
 	 (* We register the infos *)
 	 List.iter
-	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
+	   (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id)))
 	   expr_list)
 
 let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index a82a8b360..33420d813 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -16,7 +16,7 @@ val functional_induction :
   EConstr.constr ->
   (EConstr.constr * EConstr.constr bindings) option ->
   Tacexpr.or_and_intro_pattern option ->
-  Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
+  Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
 
 
 val make_graph :  Globnames.global_reference -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 8f62231ae..7558ac7ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -109,7 +109,7 @@ let const_of_id id =
   try Constrintern.locate_reference princ_ref
   with Not_found ->
     CErrors.user_err ~hdr:"IndFun.const_of_id"
-      (str "cannot find " ++ Nameops.pr_id id)
+      (str "cannot find " ++ Id.print id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
@@ -217,14 +217,14 @@ let with_full_print f a =
 
 type function_info =
     {
-      function_constant : constant;
+      function_constant : Constant.t;
       graph_ind : inductive;
-      equation_lemma : constant option;
-      correctness_lemma : constant option;
-      completeness_lemma : constant option;
-      rect_lemma : constant option;
-      rec_lemma : constant option;
-      prop_lemma : constant option;
+      equation_lemma : Constant.t option;
+      correctness_lemma : Constant.t option;
+      completeness_lemma : Constant.t option;
+      rect_lemma : Constant.t option;
+      rec_lemma : Constant.t option;
+      prop_lemma : Constant.t option;
       is_general : bool; (* Has this function been defined using general recursive definition *)
     }
 
@@ -389,7 +389,7 @@ let update_Function finfo =
 			 
 
 let add_Function is_general f =
-  let f_id = Label.to_id (con_label f) in
+  let f_id = Label.to_id (Constant.label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
   and correctness_lemma = find_or_none (mk_correct_id f_id)
   and completeness_lemma = find_or_none (mk_complete_id f_id)
@@ -548,5 +548,5 @@ let compose_prod l b = prodn (List.length l) l b
 
 type tcc_lemma_value = 
   | Undefined
-  | Value of Constr.constr
+  | Value of Term.constr
   | Not_needed
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index aa42b2ab9..6b40c9171 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -23,7 +23,7 @@ val array_get_start : 'a array -> 'a array
 val id_of_name : Name.t -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> constant
+val locate_constant : Libnames.reference -> Constant.t
 val locate_with_msg :
   Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
   Libnames.reference -> 'a
@@ -70,21 +70,21 @@ val with_full_print : ('a -> 'b) -> 'a -> 'b
 
 type function_info =
     {
-      function_constant : constant;
+      function_constant : Constant.t;
       graph_ind : inductive;
-      equation_lemma : constant option;
-      correctness_lemma : constant option;
-      completeness_lemma : constant option;
-      rect_lemma : constant option;
-      rec_lemma : constant option;
-      prop_lemma : constant option;
+      equation_lemma : Constant.t option;
+      correctness_lemma : Constant.t option;
+      completeness_lemma : Constant.t option;
+      rect_lemma : Constant.t option;
+      rec_lemma : Constant.t option;
+      prop_lemma : Constant.t option;
       is_general : bool;
     }
 
-val find_Function_infos : constant -> function_info
+val find_Function_infos : Constant.t -> function_info
 val find_Function_of_graph : inductive -> function_info
 (* WARNING: To be used just after the graph definition !!! *)
-val add_Function : bool -> constant -> unit
+val add_Function : bool -> Constant.t -> unit
 
 val update_Function : function_info -> unit
 
@@ -123,5 +123,5 @@ val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
                                                         
 type tcc_lemma_value = 
   | Undefined
-  | Value of Constr.constr
+  | Value of Term.constr
   | Not_needed
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8152e181a..ebdb490e3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i =
    \end{enumerate}
 
 *)
-let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic =
+let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic =
   fun g ->
     (* first of all we recreate the lemmas types to be used as predicates of the induction principle
        that is~:
@@ -342,7 +342,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *)
       (
-	tclTHENSEQ
+	tclTHENLIST
 	  [
 	    observe_tac("h_intro_patterns ")  (let l = (List.nth intro_pats (pred i)) in 
 					       match l with 
@@ -415,7 +415,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       in
       (params_bindings@lemmas_bindings)
     in
-    tclTHENSEQ
+    tclTHENLIST
       [ 
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
@@ -468,7 +468,7 @@ let tauto =
 
 let  rec intros_with_rewrite g =
   observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-and intros_with_rewrite_aux : tactic =
+and intros_with_rewrite_aux : Proof_type.tactic =
   fun g ->
     let eq_ind = make_eq () in
     let sigma = project g in
@@ -480,16 +480,16 @@ and intros_with_rewrite_aux : tactic =
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
+			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
 		      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) 
-		      then tclTHENSEQ[
+		      then tclTHENLIST[
 			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
 			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
 		      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) 
-		      then tclTHENSEQ[
+		      then tclTHENLIST[
 			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
 			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
@@ -498,7 +498,7 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar sigma args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
+			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar sigma args.(1)) id;
 				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
@@ -507,7 +507,7 @@ and intros_with_rewrite_aux : tactic =
 		      else if isVar sigma args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
-			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
+			tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar sigma args.(2)) id;
 				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
@@ -516,7 +516,7 @@ and intros_with_rewrite_aux : tactic =
 		      else
 			begin
 			  let id = pf_get_new_id (Id.of_string "y") g  in
-			  tclTHENSEQ[
+			  tclTHENLIST[
 			    Proofview.V82.of_tactic (Simple.intro id);
 			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
@@ -525,12 +525,12 @@ and intros_with_rewrite_aux : tactic =
 		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
-		      tclTHENSEQ[
+		      tclTHENLIST[
 			Proofview.V82.of_tactic (simplest_case v);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
-		      tclTHENSEQ[
+		      tclTHENLIST[
 			Proofview.V82.of_tactic (reduce
 			  (Genredexpr.Cbv
 			     {Redops.all_flags
@@ -542,10 +542,10 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		  | _ ->
 		      let id = pf_get_new_id (Id.of_string "y") g  in
-		      tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
+		      tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
-	      tclTHENSEQ[
+	      tclTHENLIST[
 		Proofview.V82.of_tactic (reduce
 		  (Genredexpr.Cbv
 		     {Redops.all_flags
@@ -562,7 +562,7 @@ let rec reflexivity_with_destruct_cases g =
     try
       match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
-	    tclTHENSEQ[
+	    tclTHENLIST[
 	      Proofview.V82.of_tactic (simplest_case v);
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
@@ -582,7 +582,7 @@ let rec reflexivity_with_destruct_cases g =
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) t1 t2
-		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
+		     then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
     )
@@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g =
 *)
 
 
-let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
+let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic =
   fun g ->
     (* We compute the types of the different mutually recursive lemmas
        in $\zeta$ normal form
@@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
        using [f_equation] if it is recursive (that is the graph is infinite
        or unfold if the graph is finite
     *)
-    let rewrite_tac j ids : tactic =
+    let rewrite_tac j ids : Proof_type.tactic =
       let graph_def = graphs.(j) in
       let infos =
         try find_Function_infos (fst (destConst (project g) funcs.(j)))
@@ -686,7 +686,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  try Option.get (infos).equation_lemma
 	  with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.")
 	in
-	tclTHENSEQ[
+	tclTHENLIST[
 	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
 	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
@@ -722,7 +722,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	  end
       in
       let this_branche_ids = List.nth intro_pats (pred i) in
-      tclTHENSEQ[
+      tclTHENLIST[
 	(* we expand the definition of the function *)
         observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids);
 	(* introduce hypothesis with some rewrite *)
@@ -735,7 +735,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let params_names = fst (List.chop princ_infos.nparams args_names) in
     let open EConstr in
     let params = List.map mkVar params_names in
-    tclTHENSEQ
+    tclTHENLIST
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
 	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
@@ -807,7 +807,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (con_label (fst f_as_constant)) in
+	 let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
 	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	 i*)
@@ -872,7 +872,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = Label.to_id (con_label (fst f_as_constant)) in
+	 let f_id = Label.to_id (Constant.label (fst f_as_constant)) in
 	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	   i*)
@@ -923,7 +923,7 @@ let revert_graph kn post_tac hid g =
 	      | None -> tclIDTAC g
 	      | Some f_complete ->
 		  let f_args,res = Array.chop (Array.length args - 1) args in
-		  tclTHENSEQ
+		  tclTHENLIST
 		    [
 		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
 		      thin [hid];
@@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g =
    \end{enumerate}
 *)
 
-let functional_inversion kn hid fconst f_correct : tactic =
+let functional_inversion kn hid fconst f_correct : Proof_type.tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let sigma = project g in
@@ -968,7 +968,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
-	  tclTHENSEQ[
+	  tclTHENLIST [
 	    pre_tac hid;
 	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
 	    thin [hid];
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 290d0bb91..c75f7f868 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -893,7 +893,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
       locate_constant f_ref in
     try find_Function_infos (kn_of_id id)
     with Not_found ->
-      user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme")
+      user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme")
 
 (** [merge id1 id2 args1 args2 id] builds and declares a new inductive
     type called [id], representing the merged graphs of both graphs
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bd74d2cf6..20abde82f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -77,7 +77,7 @@ let def_of_const t =
 	     | _ -> raise Not_found)
        with Not_found ->
 	 anomaly (str "Cannot find definition of constant " ++
-		    (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".")
+		    (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".")
       )
      |_ -> assert false
 
@@ -172,7 +172,7 @@ let simpl_iter clause =
     clause
 
 (* Others ugly things ... *)
-let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
+let (value_f:Term.constr list -> global_reference -> Term.constr) =
   let open Term in
   fun al fterm ->
     let rev_x_id_l =
@@ -204,7 +204,7 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) =
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Constr.constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -313,7 +313,7 @@ let check_not_nested sigma forbidden e =
       | Var x ->
         if Id.List.mem x forbidden
         then user_err ~hdr:"Recdef.check_not_nested"
-               (str "check_not_nested: failure " ++ pr_id x)
+               (str "check_not_nested: failure " ++ Id.print x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Lambda(n,t,b) -> 
       begin
@@ -458,7 +458,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
 	  check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
 	  jinfo.otherS () expr_info continuation_tac expr_info g
 	with e when CErrors.noncritical e ->
-	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+	  user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id)
       end
     | Case(ci,t,a,l) -> 
       begin
@@ -683,7 +683,7 @@ let pf_typel l tac =
   introduced back later; the result is the pair of the tactic and the
   list of hypotheses that have been generalized and cleared. *)
 let mkDestructEq :
-  Id.t list -> constr -> goal sigma -> tactic * Id.t list =
+  Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list =
   fun not_on_hyp expr g ->
   let hyps = pf_hyps g in
   let to_revert =
@@ -691,7 +691,7 @@ let mkDestructEq :
       (fun decl ->
         let open Context.Named.Declaration in
         let id = get_id decl in
-        if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (get_type decl))
+        if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl))
         then None else Some id) hyps in
   let to_revert_constr = List.rev_map mkVar to_revert in
   let type_of_expr = pf_unsafe_type_of g expr in
@@ -850,7 +850,7 @@ let rec prove_le g =
       try
 	let matching_fun = 
 	  pf_is_matching g
-	    (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in 
+	    (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in
 	let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
 	in 
 	let y = 
@@ -870,7 +870,7 @@ let rec make_rewrite_list expr_info max = function
   | [] -> tclIDTAC
   | (_,p,hp)::l -> 
     observe_tac (str "make_rewrite_list") (tclTHENS
-      (observe_tac (str "rewrite heq on " ++ pr_id p ) (
+      (observe_tac (str "rewrite heq on " ++ Id.print p ) (
 	(fun g -> 
           let sigma = project g in
 	  let t_eq = compute_renamed_type g (mkVar hp) in
@@ -965,7 +965,7 @@ let rec destruct_hex expr_info acc l =
 	onNthHypId 1 (fun hp -> 
 	  onNthHypId 2 (fun p -> 
 	    observe_tac 
-	      (str "destruct_hex after " ++ pr_id hp ++ spc () ++ pr_id p)
+	      (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p)
 	      (destruct_hex expr_info ((v,p,hp)::acc) l)
 	  )
 	)
@@ -1457,7 +1457,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
 
 let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
-	 -> Constr.constr -> unit) =
+	 -> Term.constr -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
     let open CVars in
     let opacity =