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
*
Suggestion of additional syntax for intro patterns:
letouzey
2007-07-06
*
Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record
herbelin
2007-06-30
*
- Ajout de la possibilité d'utiliser la notation Record pour les
herbelin
2007-06-30
*
killing some more non-exhaustive patterns
letouzey
2007-06-26
*
Corrections dans le Print Assumption. Les definitions locales ("Let")
aspiwack
2007-05-30
*
Corrected the treatment of negative numbers for the bigZ parser. And
aspiwack
2007-05-29
*
Réaffichage des Structure/Record sous la forme Record
herbelin
2007-05-28
*
Modification of VernacScheme to handle a new scheme: Equality (equality in
vsiles
2007-05-25
*
Added Z and Q implementations with int31.
aspiwack
2007-05-21
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Correction du pretty-printing des big-int (la sous-fonction get_height
aspiwack
2007-05-15
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Prise en compte réversibilité des notations de la forme "Notation Nil := @n...
herbelin
2007-05-10
*
Nouveaux changements autour des implicites (notamment suite à
herbelin
2007-05-06
*
Suite commit 9810
herbelin
2007-04-29
*
Ajout possibilité d'options à trois mots.
herbelin
2007-04-29
*
Ajout de la possibilité de faire référence dans certains cas à un nom
herbelin
2007-04-28
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
fin des conclusions multiples
corbinea
2007-04-26
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Nouveau déplacement de constr, cette fois au niveau 8. En fait, il y a
herbelin
2007-04-11
*
Remontée de constr de 1 à 5 (pour permettre des notations entre 1 et 5
herbelin
2007-04-10
*
Mise en place d'un rafinement de compute.
jforest
2007-04-05
*
Extension to the general sequence operator (tactical). Now in addition to ...
emakarov
2007-04-02
*
Suppression des sauts de lignes superflus de Show Script (test-suite/output/T...
notin
2007-03-21
*
Add a parameter to QuestionMark evar kind to say it can be turned into an obl...
msozeau
2007-03-19
*
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...
herbelin
2007-02-24
*
Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)
herbelin
2007-02-24
*
Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.
msozeau
2007-02-16
*
Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors
herbelin
2007-02-15
*
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2007-02-13
*
Suppression de code mort
notin
2007-02-01
*
Abbreviation of order notation.
msozeau
2007-02-01
*
redirection of errors in coqide + dynamic warning printer (needed for tm_egg)
corbinea
2007-01-31
*
Fix order of wf and measure arguments, patch Program doc.
msozeau
2007-01-31
*
"suffices" implemented + syntax cleanup
corbinea
2007-01-28
*
decl mode: anonymous facts
corbinea
2007-01-25
*
Correction du bug #1315:
notin
2007-01-22
*
changes in declarative language : by term using tactic
corbinea
2007-01-22
*
Petit oubli dans commit 9474
herbelin
2007-01-11
*
Merge from Lionel Elie Mamane's private branch:
lmamane
2007-01-10
*
Nouvelle approche pour le discharge modulaire
herbelin
2007-01-10
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
nouvelle indentation des scripts
barras
2006-12-12
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Suite ajout option -output-context
herbelin
2006-12-08
*
Ajout d'une option -output-context qui affiche le contexte en CCI pur à la
herbelin
2006-12-08
*
Remplacement de la dépendance de G_vernac en G_constr (source
herbelin
2006-12-03
*
Correction boucle du parseur en cas de caractÃère non unicode
herbelin
2006-11-20
*
Suppression du type 'tac dans les abstract_argument_type: devenu inutile
herbelin
2006-11-20
[next]