index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
q_coqast.ml4
Commit message (
Expand
)
Author
Age
*
Nouvelle mouture du traducteur v7->v8
herbelin
2003-08-11
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-06-10
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
*
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-21
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout cas Match
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Légère amélioration des messages d'erreur des with-bindings et des Rewrite
herbelin
2002-12-21
*
Ajout Simpl et Change sur des sous-termes
herbelin
2002-12-09
*
Restauration échappement ML
herbelin
2002-11-14
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
fix forbidden currified constructors
ddr
2002-11-07
*
Ajout d'un suffixe "as [ names ]" pour nommer manuellement les
herbelin
2002-10-21
*
NewDestruct/NewInduction acceptent l'option "using"
herbelin
2002-10-21
*
L'application de ltac attend une référence; meilleure protection contre
herbelin
2002-10-14
*
Première proposition d'un type ML exprimant la syntaxe de constr; nettoyage
herbelin
2002-10-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
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
*
GROS COMMIT:
barras
2001-11-05
*
Pour contourner un bug de camlp4 3.02
herbelin
2001-08-10
*
Parsing
herbelin
2001-08-10
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
entetes
filliatr
2001-03-15
*
Ajout d'un .:/opt/kde/bin:/home/herbelin/bin:/bin:/sbin:/usr/bin:/usr/etc:/us...
herbelin
2000-11-24
*
Nettoyage des fichiers de parsing
herbelin
2000-01-13
*
Restructuration printer et parser
herbelin
2000-01-07
*
compilation des grammaires (ouf)
filliatr
1999-09-08
*
modules grammaire Coq
filliatr
1999-09-08