index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
g_vernacnew.ml4
Commit message (
Expand
)
Author
Age
*
New command: "Print Ltac qualid" to print user defined tactics.
sacerdot
2005-05-20
*
Affinements suite à extension Tactic Notation aux tacticielles
herbelin
2005-05-17
*
Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...
herbelin
2005-05-17
*
Implementation of a new backtracking system, that allow to go back
coq
2005-04-20
*
Renaming Print Canonical Structure into Print Canonical Projections
herbelin
2005-02-18
*
Ajout Print Canonical Structures
herbelin
2005-02-12
*
Ajout de la syntaxe du reset label: "BackTo n".
coq
2005-01-14
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
Bug commit 1.71
herbelin
2004-11-22
*
compatibility with POWERPC
gregoire
2004-11-22
*
'Rewrite' mot-clé pour que 'Print Rewrite HintDb' marche
herbelin
2004-11-20
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...
herbelin
2004-10-12
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Nouvelle en-tête
herbelin
2004-07-16
*
Utilisation de '..' pour la notation concrete des motifs recursifs de filtrage
herbelin
2004-03-17
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
herbelin
2004-03-03
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
Correction oubli de report d'une modification de g_vernac (1.69) vers g_verna...
herbelin
2004-02-21
*
Uniformisation du comportement de Notation et Reserved Notation
herbelin
2004-02-13
*
Suppression de 'Print.' en v8
herbelin
2004-01-29
*
Réutilisation de VernacSyntacticDefinition pour différencier "Notation id :...
herbelin
2004-01-29
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
Suppression 'Implicit Arguments On/Off' qui n'a plus lieu d'etre en v8
herbelin
2004-01-20
*
Reflet dans l'arbre de syntaxe de la difference syntaxique entre 'Variables a...
herbelin
2004-01-13
*
bugs avec Pose et Assert
barras
2004-01-09
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
*** empty log message ***
barras
2003-12-23
*
Protection contre les notations vides
herbelin
2003-11-26
*
Traduction de tactic:constrarg en constr:constr pour les arguments de Tactic ...
herbelin
2003-11-26
*
Prise en compte des definitions locales dans les (co-)points-fixes
herbelin
2003-11-23
*
Ajout Print Implicit
herbelin
2003-11-21
*
Pas d'entrees autres que les predefinies en v8
herbelin
2003-11-21
*
Code mort
herbelin
2003-11-18
*
moins unaire au niveau 35, tactiques simple_induction et simple_destruct, Loc...
barras
2003-11-13
*
Suppression du "..." final !
herbelin
2003-11-12
*
petits changements de syntaxe
barras
2003-11-12
*
Suppression SearchNamed finalement redondant avec SearchAbout
herbelin
2003-11-10
*
Fusion de l'univers et du nom d'entree en un 'Print Grammar entry' en v8
herbelin
2003-11-01
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Independance de grammar.cmo vis a vis de Search; reorganisation VernacDefinition
herbelin
2003-10-23
*
Integration de SearchNamed dans SearchAbout
herbelin
2003-10-22
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Bug mot-cle TYPES
herbelin
2003-10-17
*
Changement 'as notation' en 'where notation'
herbelin
2003-10-14
[next]