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
*
Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'une
herbelin
2002-10-14
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...
herbelin
2002-10-13
*
réparation de la protection contre les clauses indiscernables de TACTIC EXTE...
herbelin
2002-10-12
*
Notation 2:Check et 2:Eval
herbelin
2002-10-12
*
Restriction sur la forme des Syntactic Definition et re-localisation en fonct...
herbelin
2002-10-12
*
Lazy manuelles dans le code
coq
2002-10-07
*
Lazy experimentale temporaire...
coq
2002-10-05
*
pretty s'appellait prettyp mais il est revenu sous son ancien nom
herbelin
2002-10-05
*
passage a ocaml 3.06
herbelin
2002-09-27
*
Un peu (plus) d'ordre dans Nametab...
coq
2002-09-24
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Pretty-printing preliminaire des modules, commandes
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Réparation d'un bug qui considérait les composantes d'un QUALID
herbelin
2002-07-30
*
Pb de factorisation camlp4
herbelin
2002-07-15
*
Pour assurer une compatibilite avec la 7.3
herbelin
2002-07-15
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Coercion de la syntaxe des motifs non atomiques
herbelin
2002-06-19
*
Petits beug d'affichages.
gregoire
2002-06-13
*
Correction mauvais ordre dans le parsing des dirpath; MAJ de la quotification
herbelin
2002-06-05
*
Fusion entre la nouvelle et l'ancienne syntaxe de HintDestruct
herbelin
2002-06-05
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Finalement un seul constr pour l'instant dans ExtraRedExpr
herbelin
2002-05-30
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Implante la macro camlp4 VERNAC COMMAND EXTEND
herbelin
2002-05-29
*
Implante la macro camlp4 TACTIC EXTEND
herbelin
2002-05-29
*
Ajout de Eval, Inst et Check
delahaye
2002-05-27
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Utilisation d'une construction spéciale SECVAR pour gérer la
herbelin
2002-05-14
*
Plus de souplesse pour les constructeurs encapsulés sous des définitions
herbelin
2002-05-10
*
Suppression d'un warning plus surprenant qu'utile
herbelin
2002-04-18
*
Typo
herbelin
2002-04-16
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
Syntactic Definition autorisée dans les motifs de Cases (utile notamment
herbelin
2002-04-10
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Correction bug infix sur des varaiables
mohring
2002-03-29
*
Ajout de l'entrée ne_constrarg_list
delahaye
2002-03-19
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
substitution et pattern modulo let
barras
2002-02-11
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Bug affichage '++' au lieu de ';'
herbelin
2001-12-21
[next]