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

2 files changed, 46 insertions, 2 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 1257044d35..ffe53e505f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -281,3 +281,37 @@ let declare_mind isrecord mie =
   !xml_declare_inductive (isrecord,oname);
   oname
 
+(* Declaration messages *)
+
+let pr_rank i = str (ordinal (i+1))
+
+let fixpoint_message indexes l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "no recursive definition"
+  | [id] -> pr_id id ++ str " is recursively defined" ++
+      (match indexes with
+	 | Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
+	 | _ -> mt ())
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+		  spc () ++ str "are recursively defined" ++
+		  match indexes with
+		    | Some a -> spc () ++ str "(decreasing respectively on " ++
+			prlist_with_sep pr_coma pr_rank (Array.to_list a) ++
+			str " arguments)"
+		    | None -> mt ()))
+
+let cofixpoint_message l =
+  Flags.if_verbose msgnl (match l with
+  | [] -> anomaly "No corecursive definition."
+  | [id] -> pr_id id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+                    spc () ++ str "are corecursively defined"))
+
+let recursive_message isfix i l =
+  (if isfix then fixpoint_message i else cofixpoint_message) l
+
+let definition_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is defined")
+
+let assumption_message id =
+  Flags.if_verbose msgnl (pr_id id ++ str " is assumed")
diff --git a/library/declare.mli b/library/declare.mli
index 1a68f8e201..09526f341f 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -59,10 +59,20 @@ val declare_internal_constant :
    the whole block (boolean must be true iff it is a record) *)
 val declare_mind : bool -> mutual_inductive_entry -> object_name
 
-(* hooks for XML output *)
+(* Hooks for XML output *)
 val set_xml_declare_variable : (object_name -> unit) -> unit
 val set_xml_declare_constant : (bool * constant -> unit) -> unit
 val set_xml_declare_inductive : (bool * object_name -> unit) -> unit
 
-(* hook for the cache function of constants and inductives *)
+(* Hook for the cache function of constants and inductives *)
 val add_cache_hook : (full_path -> unit) -> unit
+
+(* Declaration messages *)
+
+val definition_message : identifier -> unit
+val assumption_message : identifier -> unit
+val fixpoint_message : int array option -> identifier list -> unit
+val cofixpoint_message : identifier list -> unit
+val recursive_message : bool (* true = fixpoint *) ->
+  int array option -> identifier list -> unit
+