index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
theories
/
Init
Commit message (
Expand
)
Author
Age
*
Datatypes.length and app defined back via fun+fix instead of Fixpoint
letouzey
2009-11-06
*
Better visibility of the inductive CompSpec used to specify comparison functions
letouzey
2009-11-03
*
Remove various useless {struct} annotations
letouzey
2009-11-02
*
list, length, app are migrated from List to Datatypes
letouzey
2009-11-02
*
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
letouzey
2009-10-08
*
Implicit argument of Logic.eq become maximally inserted
letouzey
2009-10-08
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
New tactic to rewrite decidability lemmas when one knows which side
herbelin
2009-08-24
*
Fixed extra space in printing notation { x & P } + minor other things
herbelin
2009-08-11
*
OrderedTypeEx.N_as_OT use Nlt, various minor improvements in N/ZArith
letouzey
2009-07-24
*
Miscellaneous practical commits:
herbelin
2009-06-29
*
Parsing files for numerals (+ ascii/string) moved into plugins
letouzey
2009-03-27
*
Better mechanism for loading initial plugins
letouzey
2009-03-14
*
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2009-01-02
*
Switched to "standardized" names for the properties of eq and
herbelin
2009-01-01
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
*
- Optimized "auto decomp" which had a (presumably) exponential in
herbelin
2008-12-26
*
Fine-tuning rewriting from "eq_true b": using <- to rewrite true to b
herbelin
2008-11-23
*
- Fixed minor bug #1994 in the tactic chapter of the manual [doc]
herbelin
2008-11-22
*
ugly comment erroneously left in the minus definition
letouzey
2008-10-14
*
Correction de bugs:
herbelin
2008-08-05
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the
herbelin
2008-07-23
*
Changing the definitions of pred and minus in the style of GG
werner
2008-06-12
*
- Patch sur "intros until 0"
herbelin
2008-06-08
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Petites corrections diverses :
herbelin
2008-06-02
*
- Modification de la déf de minus et pred conformément aux remarques de
herbelin
2008-05-28
*
Notation concise pour la valeur par défaut des cas reconnus comme
herbelin
2008-05-28
*
MAJ et bricoles diverses
herbelin
2008-05-12
*
Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]
herbelin
2008-05-09
*
Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la
herbelin
2008-04-29
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23
*
contradict can now handle False hypothesis in the spirit of contradiction
letouzey
2008-04-09
*
Nettoyage Wf.v et unification (suite remarques faites sur cocorico)
herbelin
2008-03-23
*
Une passe sur les réels:
herbelin
2008-03-23
*
Do a second pass on the treatment of user-given implicit arguments. Now
msozeau
2008-03-15
*
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-03-07
*
still one more substituion s/Set/Type/
letouzey
2008-03-04
*
Proper implicit arguments handling for assumptions
msozeau
2008-02-26
*
Typo
notin
2008-01-23
*
Quelques arguments en plus...
glondu
2007-12-17
*
Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.
emakarov
2007-11-08
*
small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is
letouzey
2007-11-06
*
Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...
letouzey
2007-11-06
*
A way to specialize universally quantified hypothesis: if H is
letouzey
2007-11-01
*
Added the automatic generation of the boolean equality if possible and the
vsiles
2007-10-05
*
Révision de theories/Logic concernant les axiomes de descriptions.
herbelin
2007-10-03
*
Ajout infos de débogage de "universe inconsistency" quand option Set
herbelin
2007-09-30
[next]