Restructuration of command.ml + generic infrastructure for inductive schemes

- Cleaning and uniformisation in command.ml:
  - For better modularity and better visibility, two files got isolated
    out of command.ml:
    - lemmas.ml is about starting and saving a proof
    - indschemes.ml is about declaring inductive schemes
  - Decomposition of the functions of command.ml into a functional part
    and the imperative part
- Inductive schemes:
  - New architecture in ind_tables.ml for registering scheme builders,
    and for sharing and generating on demand inductive schemes
  - Adding new automatically generated equality schemes (file eqschemes.ml)
    - "_congr" for equality types (completing here commit 12273)
    - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
      "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
      rewriting schemes (warning, rew_forward_dep cannot be stated following
      the standard Coq pattern for inductive types: "t=u" cannot be the
      last argument of the scheme)
    - "_case", "_case_nodep", "_case_dep" for case analysis schemes
  - Preliminary step towards discriminate and injection working on any
    equality-like type (e.g. eq_true)
  - Restating JMeq_congr under the canonical form of congruence schemes
  - Renamed "Set Equality Scheme" into "Set Equality Schemes"
  - Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
  - Activation of the automatic generation of boolean equality lemmas
  - Partial debug and error messages improvements for the generation of
    boolean equality and decidable equality
  - Added schemes for making dependent rewrite working (unfortunately with
    not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning

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

16 files changed, 82 insertions, 79 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 949150ba54..3d789b92ed 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -968,7 +968,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	)
       ]
   in
-  Command.start_proof
+  Lemmas.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
@@ -977,7 +977,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     lemma_type
     (fun _ _ -> ());
   Pfedit.by (prove_replacement);
-  Command.save_named false
+  Lemmas.save_named false
 
 
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f6959d77e1..ff4d1e972f 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -303,7 +303,7 @@ let pp_dur time time' =
 (* let qed () = save_named true  *)
 let defined () =
   try
-    Command.save_named false
+    Lemmas.save_named false
   with
     | UserError("extract_proof",msg) ->
 	Util.errorlabstrm
@@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
-    Command.start_proof
+    Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
@@ -529,15 +529,14 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     List.map
       (fun (idx) ->
 	 let ind = first_fun_kn,idx in
-	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort
+	 ind,true,prop_sort
       )
       funs_indexes
   in
   let l_schemes =
     List.map
       (Typing.type_of env sigma)
-      (Indrec.build_mutual_indrec env sigma ind_list)
+      (Indrec.build_mutual_induction_scheme env sigma ind_list)
   in
   let i = ref (-1) in
   let sorts =
@@ -712,7 +711,7 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	 ind,prop_sort
   in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in
+  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun) in
   let sorts =
     (fun (_,_,x) ->
        Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 68850603ba..77389681b3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -150,7 +150,7 @@ let rec abstract_rawconstr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
 (*   Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
-  Constrintern.intern_gen false sigma env ~impls:([],impls)
+  Constrintern.intern_gen false sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 
@@ -166,15 +166,12 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
-        let arityc = Command.generalize_constr_expr arityc bl in
+        let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
-	let impl =
-	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits  env0 arity
-	  else [] in
-	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
-        (Environ.push_named (recname,None,arity) env, impls'))
+	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
+        (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls))
       (env0,[]) lnameargsardef in
+  let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
@@ -367,16 +364,15 @@ let generate_principle  on_error
 let register_struct is_rec fixpoint_exprl =
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+	let ce,imps =
+	  Command.interp_definition
+	    (Flags.boxed_definitions ()) bl None body (Some ret_type)
+	in
 	Command.declare_definition
-	  fname
-	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
-	  bl
-	  None
-  	  body
-	  (Some ret_type)
-	  (fun _ _ -> ())
+	  fname (Decl_kinds.Global,Decl_kinds.Definition)
+	  ce imps (fun _ _ -> ())
     | _ ->
-	Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
+	Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
 
 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
@@ -389,7 +385,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Command.generalize_constr_expr ret_type args in
+  let type_of_f = Topconstr.prod_constr_expr ret_type args in
   let rec_arg_num =
     let names =
       List.map
@@ -420,7 +416,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Command.generalize_constr_expr unbounded_eq args in
+  let eq = Topconstr.prod_constr_expr unbounded_eq args in
   let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
       nb_args relation =
     try
@@ -531,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 			 raise (UserError("",str "Cannot find argument " ++
 					    Ppconstr.pr_id id))
 		     in
- 		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation)
+		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation option)
 		 | (name,None,args,types,body),recdef ->
 		     let names =  (Topconstr.names_of_local_assums args) in
 		     if  is_one_rec recdef  && List.length names > 1 then
@@ -541,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 		     else
 		       let loc, na = List.hd names in
 			 (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
-		     (None:Vernacexpr.decl_notation)
+		     (None:Vernacexpr.decl_notation option)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
 		     error
 		       ("Cannot use mutual definition with well-founded recursion or measure")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 116a3c9913..ca93056ad1 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -734,7 +734,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Command.save_named false
+let do_save () = Lemmas.save_named false
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
@@ -786,7 +786,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
@@ -823,10 +823,10 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let  mib,mip = Global.lookup_inductive graph_ind in
     let schemes =
       Array.of_list
-	(Indrec.build_mutual_indrec (Global.env ()) Evd.empty
+	(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i mip -> (kn,i),mib,mip,true,InType)
+		 (fun i _ -> (kn,i),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
@@ -838,7 +838,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 8aeff61e6a..6dc36decf3 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -904,7 +904,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
     } in *)
   let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
+  let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in
+  let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+  (* Declare the mutual inductive block with its associated schemes *)
+  ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
 
 
 (* Find infos on identifier id. *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 4bd0385caa..607734f222 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1364,7 +1364,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5499425dfb..d64b9728b4 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,8 +52,8 @@ open Genarg
 let compute_renamed_type gls c =
   rename_bound_var (pf_env gls) [] (pf_type_of gls c)
 
-let qed () = Command.save_named true
-let defined () = Command.save_named false
+let qed () = Lemmas.save_named true
+let defined () = Lemmas.save_named false
 
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
@@ -993,7 +993,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       )
       		 g)
 ;
-    Command.save_named opacity;
+    Lemmas.save_named opacity;
   in
   start_proof
     na
@@ -1042,7 +1042,7 @@ let com_terminate
     nb_args
     hook =
   let start_proof (tac_start:tactic) (tac_end:tactic) =
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     start_proof thm_name
       (Global, Proof Lemma) (Environ.named_context_val env)
       (hyp_terminates nb_args fonctional_ref) hook;
@@ -1322,7 +1322,7 @@ let (com_eqn : identifier ->
 	    else begin match cb.const_body with None -> true | _ -> false end
 	| _ -> anomaly "terminate_lemma: not a constant"
     in
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = (constr_of_global f_ref) in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
@@ -1343,7 +1343,7 @@ let (com_eqn : identifier ->
        );
 (*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () ->Command.save_named opacity) () ;
+     Flags.silently (fun () -> Lemmas.save_named opacity) () ;
 (*      Pp.msgnl (str "eqn finished"); *)
 
     );;
@@ -1358,7 +1358,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
 (*   Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
-  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in
+  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq in
 (*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in
diff --git a/plugins/interface/centaur.ml4 b/plugins/interface/centaur.ml4
index 07f32b6d43..019ffdbe72 100644
--- a/plugins/interface/centaur.ml4
+++ b/plugins/interface/centaur.ml4
@@ -787,9 +787,9 @@ let output_depends compute_depends ptree =
 
 let gen_start_depends_dumps print_depends print_depends' print_depends'' print_depends''' =
   Command.set_declare_definition_hook (print_depends' (Depends.depends_of_definition_entry ~acc:[]));
-  Command.set_declare_assumption_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
-  Command.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
-  Command.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
+  Command.set_declare_assumptions_hook (print_depends  (fun (c:types) -> Depends.depends_of_constr c []));
+  Lemmas.set_start_hook (print_depends    (fun c -> Depends.depends_of_constr c []));
+  Lemmas.set_save_hook  (print_depends''  (Depends.depends_of_pftreestate Depends.depends_of_pftree));
   Refiner.set_solve_hook (print_depends''' (fun pt -> Depends.depends_of_pftree_head pt []))
 
 let start_depends_dumps () = gen_start_depends_dumps output_depends output_depends output_depends output_depends
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 85b55f36c4..96bda6eccc 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -75,10 +75,10 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let evm, c, typ, imps =
-    Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None
+    Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr t bl) None
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
-    Command.start_proof id kind c (fun loc gr ->
+    Lemmas.start_proof id kind c (fun loc gr ->
       Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
       hook loc gr)
 
@@ -93,14 +93,14 @@ let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("An
 let assumption_message id =
   Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
-let declare_assumption env isevars idl is_coe k bl c nl =
+let declare_assumptions env isevars idl is_coe k bl c nl =
   if not (Pfedit.refining ()) then
     let id = snd (List.hd idl) in
     let evm, c, typ, imps =
-      Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None
+      Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
+      List.iter (Command.declare_assumption is_coe k c imps false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
@@ -119,7 +119,7 @@ let vernac_assumption env isevars kind l nl =
 	List.iter (fun lid ->
 	  if global then Dumpglob.dump_definition lid (not global) "ax"
 	  else dump_variable lid) idl;
-      declare_assumption env isevars idl is_coe kind [] c nl) l
+      declare_assumptions env isevars idl is_coe kind [] c nl) l
 
 let check_fresh (loc,id) =
   if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index c47a1c4c4d..26ac445c32 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -114,7 +114,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
   in
   let tclass = if generalize then CGeneralization (dummy_loc, Implicit, Some AbsPi, tclass) else tclass in
   let k, ctx', imps, subst =
-    let c = Command.generalize_constr_expr tclass ctx in
+    let c = Topconstr.prod_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
     let ctx, c = decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app (push_rel_context ctx env) c in
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 2a31d4e18d..007013d405 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -294,13 +294,10 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   let lift_lets = Termops.lift_rel_context 1 letbinders in
   let intern_body =
     let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
-    let impls = Command.compute_interning_datas env Constrintern.Recursive [] [recname] [full_arity] [impls] in
-    let newimpls =
-      match snd impls with
-      [(p, (r, l, impls, scopes))] ->
-	[(p, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))]
-      | x -> x
-    in interp_casted_constr isevars ~impls:(fst impls,newimpls)
+    let (r, l, impls, scopes) = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in
+    let newimpls = [(recname, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))] in
+    let newimpls = Constrintern.set_internalization_env_params newimpls [] in
+    interp_casted_constr isevars ~impls:newimpls
       (push_rel_context ctx env) body (lift 1 top_arity)
   in
   let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
@@ -412,7 +409,7 @@ let check_evars env initial_sigma evd c =
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
-  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
+  let kind = fixkind <> IsCoFixpoint in
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -433,13 +430,13 @@ let interp_recursive fixkind l boxed =
   let env_rec = push_named_context rec_sign env in
 
   (* Get interpretation metadatas *)
-  let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in
+  let impls = Constrintern.compute_full_internalization_env env Constrintern.Recursive [] fixnames fixtypes fiximps in
   let notations = List.fold_right Option.List.cons ntnl [] in
 
   (* Interp bodies with rollback because temp use of notations/implicit *)
   let fixdefs =
     States.with_state_protection (fun () ->
-      List.iter (Command.declare_interning_data impls) notations;
+      List.iter (Metasyntax.set_notation_for_interpretation impls) notations;
       list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
       () in
 
@@ -478,7 +475,7 @@ let interp_recursive fixkind l boxed =
   in
   let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
     (match fixkind with
-      | Command.IsFixpoint wfl ->
+      | IsFixpoint wfl ->
 	  let possible_indexes =
 	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
 	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
@@ -487,7 +484,7 @@ let interp_recursive fixkind l boxed =
 	  in
 	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
 	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
-      | Command.IsCoFixpoint -> ());
+      | IsCoFixpoint -> ());
     Subtac_obligations.add_mutual_definitions defs notations fixkind
 
 let out_n = function
@@ -511,7 +508,7 @@ let build_recursive l b =
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
 	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) ->
 	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l
-	  in interp_recursive (Command.IsFixpoint g) fixl b
+	  in interp_recursive (IsFixpoint g) fixl b
       | _, _ ->
 	  errorlabstrm "Subtac_command.build_recursive"
 	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
@@ -520,4 +517,4 @@ let build_corecursive l b =
   let fixl = List.map (fun (((_,id),bl,typ,def),ntn) ->
     ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
     l in
-  interp_recursive Command.IsCoFixpoint fixl b
+  interp_recursive IsCoFixpoint fixl b
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 6c0c4340f9..c9064ec822 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -13,7 +13,7 @@ val interp_gen :
   typing_constraint ->
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   ?allow_patvar:bool ->
   ?ltacvars:ltac_sign ->
   constr_expr -> constr
@@ -23,12 +23,12 @@ val interp_constr :
 val interp_type_evars :
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   constr_expr -> constr
 val interp_casted_constr_evars :
   evar_defs ref ->
   env ->
-  ?impls:full_implicits_env ->
+  ?impls:full_internalization_env ->
   constr_expr -> types -> constr
 val interp_open_constr :
   evar_defs ref -> env -> constr_expr -> constr
@@ -54,7 +54,7 @@ val build_wellfounded :
            Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
 
 val build_recursive :
-  (fixpoint_expr * decl_notation) list -> bool -> unit
+  (fixpoint_expr * decl_notation option) list -> bool -> unit
 
 val build_corecursive :
-  (cofixpoint_expr * decl_notation) list -> bool -> unit
+  (cofixpoint_expr * decl_notation option) list -> bool -> unit
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 9b0b39cf82..45dfc44bcb 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -45,6 +45,10 @@ type obligation =
 
 type obligations = (obligation array * int)
 
+type fixpoint_kind =
+  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsCoFixpoint
+
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
 type program_info = {
@@ -53,7 +57,7 @@ type program_info = {
   prg_type: constr;
   prg_obligations: obligations;
   prg_deps : identifier list;
-  prg_fixkind : Command.fixpoint_kind option ;
+  prg_fixkind : fixpoint_kind option ;
   prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
@@ -288,8 +292,8 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let kns = list_map4 (declare_fix boxed kind) fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
-    List.iter (Command.declare_interning_data ([],[])) first.prg_notations;
-    Flags.if_verbose ppnl (Command.recursive_message kind indexes fixnames);
+    List.iter Metasyntax.add_notation_interpretation first.prg_notations;
+    Declare.recursive_message (fixkind<>IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
       first.prg_hook local gr;
@@ -435,7 +439,7 @@ let rec solve_obligation prg num =
       match deps_remaining obls obl.obl_deps with
       | [] ->
 	  let obl = subst_deps_obl obls obl in
-	    Command.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
+	    Lemmas.start_proof obl.obl_name (kind_of_opacity obl.obl_status) obl.obl_type
 	      (fun strength gr ->
 		let cst = match gr with ConstRef cst -> cst | _ -> assert false in
 		let obl =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 04e2371af7..2666430a8f 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -29,6 +29,10 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types ->
 
 type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list
 
+type fixpoint_kind =
+  | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list
+  | IsCoFixpoint
+
 val add_mutual_definitions :
   (Names.identifier * Term.constr * Term.types *
       (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
@@ -36,7 +40,7 @@ val add_mutual_definitions :
   ?kind:Decl_kinds.definition_kind ->
   ?hook:Tacexpr.declaration_hook ->
   notations ->
-  Command.fixpoint_kind -> unit
+  fixpoint_kind -> unit
 
 val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit
 
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 11a9fa9f53..e2910b8c41 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -110,12 +110,12 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id bl c tycon =
-  let c = Command.abstract_constr_expr c bl in
+  let c = Topconstr.abstract_constr_expr c bl in
   let tycon =
     match tycon with
 	None -> empty_tycon
       | Some t ->
-	  let t = Command.generalize_constr_expr t bl in
+	  let t = Topconstr.prod_constr_expr t bl in
 	  let t = coqintern_type !isevars env t in
 	  let coqt, ttyp = interp env isevars t empty_tycon in
 	    mk_tycon coqt
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index fbe40525bd..64f5fe9c73 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -323,7 +323,7 @@ let and_tac l hook =
 	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
   in
   let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
-    Command.start_proof and_proofid goal_kind and_goal
+    Lemmas.start_proof and_proofid goal_kind and_goal
       (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
     trace (str "Started and proof");
     Pfedit.by and_tac;