index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
CHANGES
Commit message (
Expand
)
Author
Age
*
MAJ
herbelin
2005-12-21
*
Declare Implicit Tactic
herbelin
2005-09-09
*
add a left and right tactic for classical logic
narboux
2005-07-15
*
fold
herbelin
2005-07-15
*
Added entry constr_may_eval for tactic extensions (new syntax)
herbelin
2005-06-22
*
New environment variable COQREMOTEBROWSER to set the command used by Coq
sacerdot
2005-05-26
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Implemented autorewrite with ... in hyp [using ...].
sacerdot
2005-05-18
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
possibilité d'écrire [foo| ] au lieu de [foo|idtac]
letouzey
2005-05-09
*
Fixed hypotheses of Z_lt_induction (see #957)
herbelin
2005-04-26
*
Missing translating a 'O' into a '0' (again - cf bug #947); removed useless h...
herbelin
2005-03-29
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
HUGE COMMIT
sacerdot
2005-01-03
*
Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)
herbelin
2004-12-27
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
MAJ
herbelin
2004-11-09
*
Prise en compte des notations récursives dans l'option 'format'
herbelin
2004-11-08
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
Ajout de or-pattern pour le match-with v8
herbelin
2004-09-09
*
Incorrection exportation XML
herbelin
2004-04-17
*
Finalement pas de liste des contributions (cela n'avait été fait que pour l...
herbelin
2004-04-17
*
Nouvelles majs
herbelin
2004-04-16
*
MAJ
herbelin
2004-04-14
*
MAJ
herbelin
2004-03-28
*
MAJ
herbelin
2004-03-17
*
preparation pour release (suite)
barras
2004-03-15
*
MAJ
herbelin
2004-03-15
*
MAJ
herbelin
2004-03-10
*
MAJ
herbelin
2004-02-27
*
MAJ
herbelin
2004-02-21
*
MAJ
herbelin
2004-02-12
*
New version of Functional Scheme and functional induction. Deals with
coq
2004-02-09
*
MAJ
herbelin
2004-02-06
*
MAJ
herbelin
2004-02-03
*
MAJ
herbelin
2004-01-29
*
MAJ
herbelin
2004-01-23
*
MAJ
herbelin
2004-01-21
*
*** empty log message ***
barras
2003-12-23
*
MAJ
herbelin
2003-12-22
*
*** empty log message ***
clrenard
2003-12-01
*
Nouvelle tactique EExists
clrenard
2003-12-01
*
Idtac parle
narboux
2003-12-01
*
MAJ
herbelin
2003-11-30
[next]