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

1 files changed, 13 insertions, 6 deletions

diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 53822b473..01c0a34da 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Util
+open Names
 open Libnames
 open Ppextend
 open Extend
@@ -41,20 +42,26 @@ val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
 (* Add only the interpretation of a notation that already has pa/pp rules *)
 
-val add_notation_interpretation : string -> Constrintern.implicits_env ->
-  constr_expr -> scope_name option -> unit
+val add_notation_interpretation :
+  (string * constr_expr * scope_name option) -> unit
+
+(* Add a notation interpretation for supporting the "where" clause *)
+
+val set_notation_for_interpretation : Constrintern.full_internalization_env ->
+  (string * constr_expr * scope_name option) -> unit
 
 (* Add only the parsing/printing rule of a notation *)
 
 val add_syntax_extension :
   locality_flag -> (string * syntax_modifier list) -> unit
 
-(* Print the Camlp4 state of a grammar *)
+(* Add a syntactic definition (as in "Notation f := ...") *)
 
-val print_grammar : string -> unit
+val add_syntactic_definition : identifier -> identifier list * constr_expr ->
+  bool -> bool -> unit
 
-(* Evaluate whether a notation is not printable *)
+(* Print the Camlp4 state of a grammar *)
 
-val is_not_printable : aconstr -> bool
+val print_grammar : string -> unit
 
 val check_infix_modifiers : syntax_modifier list -> unit