| Age | Commit message (Collapse) | Author |
|---|
|
- 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
|
|
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
as hints (see wish #2104).
- New type hint_entry for interpreted hint.
- Better centralization of functions dealing with evaluable_global_reference.
- Unfortunately, camlp4 does not factorize rules so that "Hint Resolve" had
uglily to be factorized by hand.
- Typography in RefMan-tac.tex.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12121 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
identity. Add notations for compatibility and support for
understanding these notations in the ml files.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11729 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
decidability of the usual equality
Major changes:
* andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v
* added 2 files:
* toplevel/ind_tables.ml* : tables where the boolean eqs and the
decidability proofs are stored
* toplevel/auto_ind_decl.ml* : code of the schemes that are automatically
generated from inductives types (currently boolean eq & decidability )
* improvement of injection: if the decidability have been correctly computed,
injection can now break the equalities over dependant pair
How to use:
Set Equality Scheme. to set the automatic generation of the equality when you
create a new inductive type
Scheme Equality for I. tries to create the equality for the already declared
type I
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conjunction of mutual inductions principles.
e.g: Combined Scheme mutind from tree_ind, forest_ind gives a conclusion (forall t : tree, P t) /\ (forall f : forest, P0 f).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fixes to the subtac implementation, utility tactic to apply existentials to a function and build a dependent sum out of name, constr lists.
Also defined a Utils coq module for tactics related to subsets and the projections for ex in Prop.
- Enhancements to inference algorithm added but not used in the default version as there are some remaining bugs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8688 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7985 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
eq_rawconstr in topconstr to prepare the introduction of the new
version of functionnal induction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7928 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6616 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dans la biblio standard
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4753 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
tactiques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4032 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
constrextern.ml est l'équivalent de termast.ml pour le nouveau
printer; topconstr.ml; contient la définition de "constr_expr";
modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
|
