From 272194ae1dd0769105e1f485c9b96670a19008a7 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 8 Nov 2009 17:31:16 +0000 Subject: 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 --- dev/base_include | 5 +++++ dev/doc/changes.txt | 28 ++++++++++++++++++++++++++++ 2 files changed, 33 insertions(+) (limited to 'dev') diff --git a/dev/base_include b/dev/base_include index b6c2e4d08f..41d1ac3bbc 100644 --- a/dev/base_include +++ b/dev/base_include @@ -53,6 +53,7 @@ open Names open Term open Typeops +open Term_typing open Univ open Inductive open Indtypes @@ -139,10 +140,14 @@ open Refine open Tacinterp open Tacticals open Tactics +open Eqschemes open Cerrors open Class open Command +open Indschemes +open Ind_tables +open Lemmas open Coqinit open Coqtop open Discharge diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index ebbcb46ce9..505141dd66 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -2,6 +2,34 @@ = CHANGES BETWEEN COQ V8.2 AND COQ V8.3 = ========================================= +** Cleaning in commmand.ml + +Functions about starting/ending a lemma are in lemmas.ml +Functions about inductive schemes are in indschemes.ml + +Functions renamed: + +declare_one_assumption -> declare_assumption +declare_assumption -> declare_assumptions +Command.syntax_definition -> Metasyntax.add_syntactic_definition +declare_interning_data merged with add_notation_interpretation +compute_interning_datas -> compute_full_internalization_env +implicits_env -> internalization_env +full_implicits_env -> full_internalization_env +build_mutual -> do_mutual_inductive +build_recursive -> do_fixpoint +build_corecursive -> do_cofixpoint +build_induction_scheme -> build_mutual_induction_scheme +build_indrec -> build_induction_scheme +instantiate_type_indrec_scheme -> weaken_sort_scheme +instantiate_indrec_scheme -> modify_sort_scheme +make_case_dep, make_case_nodep -> build_case_analysis_scheme +make_case_gen -> build_case_analysis_scheme_default + +Types: + +decl_notation -> decl_notation option + ** Cleaning in libnames/nametab interfaces Functions: -- cgit v1.2.3