index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Added support for multiple where-clauses in Inductive and co (see wish #2163).
herbelin
2009-11-11
*
Improving abbreviations/notations + backtrack of semantic change in r12439
herbelin
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Misc fixes.
msozeau
2009-11-06
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Integrate a few improvements on typeclasses and Program from the equations br...
msozeau
2009-10-28
*
Module type expressions of the form (Fsig X) with Definition foo := bar are n...
soubiran
2009-10-28
*
Add a new vernacular command for controling implicit generalization of
msozeau
2009-10-27
*
New cleaning phase of the Local/Global option management
herbelin
2009-10-26
*
Restore (and test) broken chaining of lemmas in "apply in" in presence
herbelin
2009-10-25
*
fixed bug in Czar grammar
corbinea
2009-10-25
*
Improved the treatment of Local/Global options (noneffective Local on
herbelin
2009-10-25
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Fixed a notation bug when extending binder_constr with empty levels
herbelin
2009-10-17
*
Removal of trailing spaces.
serpyc
2009-10-04
*
Add support for Local Declare ML Module
glondu
2009-09-29
*
Complement to 12347 and 12348 on the extended syntax of case/elim.
herbelin
2009-09-27
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
Add "case as/in/using" and temporary "destruct" with n args.
herbelin
2009-09-20
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Addition of "Reserved Infix" continued.
herbelin
2009-09-14
*
- Inductive types in the "using" option of auto/eauto/firstorder are
herbelin
2009-09-13
*
Generalized the possibility to refer to a global name by a notation
herbelin
2009-09-11
*
Added syntax "exists bindings, ..., bindings" for iterated "exists".
herbelin
2009-09-10
*
Postpone checking of Local/Global to allow grammar extensions to use it
msozeau
2009-09-02
*
Ajout de la gestion de Local et Global pour les options (au sens de
aspiwack
2009-08-14
*
Added profile.cmo in grammar.cma so that any functions in one of the
herbelin
2009-08-14
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
Add support for "Infix ... := constr" instead of just "Infix ... := ref".
herbelin
2009-08-11
*
Fixed incorrect optimization in Prettyp.pr_located_qualid introduced
herbelin
2009-08-07
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Added "etransitivity".
herbelin
2009-08-03
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
- Granted wish #2138 (support for local binders in syntax of Record fields).
herbelin
2009-07-15
*
Miscellaneous practical commits:
herbelin
2009-06-29
*
Allow anonymous instances again, with syntax [Instance: T] where T
msozeau
2009-06-15
*
Simplifying the call to print_no_goals and not calling it when no goal
herbelin
2009-06-11
*
- Added two new introduction patterns with the following temptative syntaxes:
herbelin
2009-06-07
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Ensure the precondition of the partial function [list_chop] holds
msozeau
2009-06-03
*
Ajout d'un printer modulaire pour les constr. C'est-à-dire une fonction
aspiwack
2009-05-28
*
Ajout d'une fonction Lexer.remove_keyword pour libérer un keyword dans
aspiwack
2009-05-27
*
=?utf-8?q?D=C3=A9sinterdiction=20de=20GDELETE=5FRULE=20dans=20pcoq.ml4.=20Mal...
aspiwack
2009-05-27
*
- Fixing declarative mode in presence of high use of Change_evars nodes
herbelin
2009-05-20
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
- Fixed a little bug in previous commit (bad failure in case of unknown entry).
herbelin
2009-04-27
*
- Cleaning (unification of ML names, removal of obsolete code,
herbelin
2009-04-27
*
- Fixing #2090 (occur check missing when trying to solve evar-evar equation).
herbelin
2009-04-25
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixing
herbelin
2009-04-08
[next]