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
*
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
*
The emacs-U option now does not output *any* char above 250.
courtieu
2006-11-17
*
Fichiers obsolètes
herbelin
2006-11-11
*
gestion speciale du niveau 5 des ltac
barras
2006-11-02
*
syntaxe du let in encore
barras
2006-10-31
*
assouplissement de la syntaxe du let de ltac: t1 ; let in autorise
barras
2006-10-31
*
fixed field_simplify + changed precedence of let and fun in ltac
barras
2006-10-30
*
Exports manquants dans ring
barras
2006-10-29
*
Compatibilité du polymorphisme de constantes avec les sections.
herbelin
2006-10-29
*
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2006-10-28
*
Documentation de "Set Printing Universes", "Print Universes" (anciennement
herbelin
2006-10-28
*
Ajout option Set Printing Universes et amélioration affichage des univers
herbelin
2006-10-28
*
Extension de la primitive ltac fresh pour qu'elle accepte une liste de
herbelin
2006-10-24
*
Hack peu élégant pour permettre de parser des listes avec séparateurs dans
herbelin
2006-10-24
*
coqide: affichage des sous-buts et hypothèses et métas comme types de
herbelin
2006-10-19
*
affichage des ... dans les scripts
barras
2006-10-16
*
Notations:
herbelin
2006-10-09
*
le parsing du LETIN ne suivait pas la DTD (bug #1237)
herbelin
2006-10-03
*
Suppression des lignes vides dans l'affichage des scripts
notin
2006-09-28
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Déplacement surround dans util.ml et parenthésage des déclarations
herbelin
2006-09-23
*
Declarative Proof Language: main commit
corbinea
2006-09-20
[next]