index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
ppvernac.ml
Commit message (
Expand
)
Author
Age
...
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Nettoyage de Print Assumptions :
aspiwack
2007-11-09
*
Modification of the Scheme command.
vsiles
2007-09-28
*
Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...
herbelin
2007-08-24
*
Corrections dans le Print Assumption. Les definitions locales ("Let")
aspiwack
2007-05-30
*
Modification of VernacScheme to handle a new scheme: Equality (equality in
vsiles
2007-05-25
*
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-05-11
*
Nouveaux changements autour des implicites (notamment suite à
herbelin
2007-05-06
*
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
*
New keyword "Inline" for Parameters and Axioms for automatic
soubiran
2007-04-25
*
Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)
herbelin
2007-02-24
*
Fix order of wf and measure arguments, patch Program doc.
msozeau
2007-01-31
*
Petit oubli dans commit 9474
herbelin
2007-01-11
*
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
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Ajout possibilité clause "where" dans co-points fixes
herbelin
2006-09-01
*
making otags working
jforest
2006-08-22
*
Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...
herbelin
2006-07-05
*
Added {measure x f} as a valid recursion order.
msozeau
2006-06-22
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
Diverses corrections de l'afficheur et du traducteur pour s'assurer de
herbelin
2006-04-26
*
Si un fixpoint a plusieurs arguments, mais un seul de type inductif,
letouzey
2006-04-14
*
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
msozeau
2006-03-13
*
Réorganisation de la structure interne des types de déclarations (decl_kinds)
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Remplacement Pp.qs par Pptactic.qsnew
herbelin
2005-12-28
*
Autres suppressions de composantes du traducteur
herbelin
2005-12-27
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
[prev]