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

8 files changed, 39 insertions, 34 deletions

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;