index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
translate
Commit message (
Expand
)
Author
Age
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
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
*
Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...
herbelin
2005-01-02
*
ExtraRedExpr maintenant sans argument: pas très souple mais au moins convien...
herbelin
2004-12-29
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
pp of nested fixpoints (dangling with/for)
barras
2004-12-01
*
Export pr_intro_pattern
herbelin
2004-11-30
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Ajout 'Locate Module'
herbelin
2004-11-17
*
Affichage des univers
herbelin
2004-11-04
*
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
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
Ajout de or-pattern pour le match-with v8
herbelin
2004-09-09
*
"Print Setoids" command added.
sacerdot
2004-07-23
*
Abstraction vis à vis du type loc pour compatibilité ocaml 3.08
herbelin
2004-07-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
more evar stuff
corbinea
2004-06-28
*
Plus de robustesse en traduisant les 'Repeat Induction' et les 'Do n Induction'
herbelin
2004-06-02
*
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-04-17
*
Chgt role 2eme argument AList et implantation affichage motifs recursifs de n...
herbelin
2004-04-08
*
code mort
herbelin
2004-03-24
*
Traduction ad hoc pour Hint Rewrite in using
herbelin
2004-03-18
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Hack pour traduction des changements non uniformes de syntaxe des TACTIC et V...
herbelin
2004-03-17
*
Mise en place de motifs récursifs dans Notation; quelques simplifications au...
herbelin
2004-03-17
*
Bug inversion abstract_constr_expr et prod_constr_expr
herbelin
2004-03-12
*
modif des fixpoints pour que si on donne une notation au produit, les pts fix...
barras
2004-03-05
*
Retablissement pour le traducteur d'une copie de pr_intro_pattern base sur la...
herbelin
2004-03-05
*
Plus de noms d'entrees de grammaires qualifies dans 'Tactic Notation'
herbelin
2004-03-03
*
Changement de natural en int_or_var pour 'do' et 'fail' pour paramétrisation...
herbelin
2004-03-02
*
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...
herbelin
2004-03-02
*
Généralisation du type ltac Identifier en IntroPattern; prise en compte des...
herbelin
2004-03-01
*
Keep structure information for Fixpoint declaration and Fix terms
bertot
2004-02-26
*
commit précédent erroné
herbelin
2004-02-20
*
Bugs/insuffisances trouvees en traduisant MMode
herbelin
2004-02-19
*
- fixed the Assert_failure error in kernel/modops
barras
2004-02-18
*
Suppression de 'Print.' en v8
herbelin
2004-01-29
*
reparation de qqs bugs du traducteur
barras
2004-01-26
*
Corrige: Intros [] etait traduit intros (), qui ne reparse pas
barras
2004-01-16
*
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
*
certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles
barras
2004-01-05
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
*** empty log message ***
barras
2003-12-24
*
Reparation semantique casse de Pose en v7
herbelin
2003-12-23
[next]