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
*
Changement de la structure des points fixes
barras
2001-05-03
*
message d'erreur pour rattrapper l'anomalie avec SQUASH
barras
2001-04-25
*
Amelioration affichage
herbelin
2001-04-25
*
Messages d'erreur Cases
herbelin
2001-04-24
*
Les clauses de Rec doivent prendre des tactic_atom's
delahaye
2001-04-24
*
un warning pas beau supprimmé
filliatr
2001-04-23
*
Petit menage
delahaye
2001-04-20
*
*** empty log message ***
mayero
2001-04-19
*
Essais dans Ltac
delahaye
2001-04-19
*
Bug affichage d'implicites pour les vars liees
herbelin
2001-04-15
*
Non parenthesage des applications de tactiques
delahaye
2001-04-14
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
Modified searchPattern. Before this correction, constructors were overlooked,
bertot
2001-04-10
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
nettoyage d'entrees de grammaires inutiles
courant
2001-04-09
*
branchement extraction en standard (pas de Require)
filliatr
2001-04-09
*
bug Print Proof; usage coqtop/coqc
filliatr
2001-04-06
*
mise en place de Correctness; vieille syntaxe Extraction viree de g_vernac.ml4
filliatr
2001-04-05
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
Add a flag to avoid sending too many warnings when reloading syntax files
bertot
2001-04-04
*
adding entry points for the arguments of the Comment command.
bertot
2001-04-04
*
Adding A command for comments, this makes it possible to have structured
bertot
2001-04-04
*
The function filter_by_module, that was previously exported was not the
bertot
2001-04-03
*
Export a function (build_inductive) that is used in the graphical interface.
bertot
2001-04-03
*
branchement extraction (bytecode seulement)
filliatr
2001-03-30
*
amelioration de la structure des univers
barras
2001-03-28
*
amelioration de la consommation memoire de la conversion en eta-expansant
barras
2001-03-23
*
Bug MUTCASE au lieu CASE
herbelin
2001-03-22
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Bug affichage coercions
herbelin
2001-02-16
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Tentative d'amélioration affichage decls locales
herbelin
2001-02-16
*
Suppression sp_of_id
herbelin
2001-02-16
*
Prise en compte noms longs dans SuperAuto
herbelin
2001-02-16
*
Prise en compte noms longs dans Implicits
herbelin
2001-02-16
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
Centralisation des références à des globaux de Coq dans Coqlib (ex-Stdlib)...
herbelin
2001-02-14
*
Bug nommage Stdlib
herbelin
2001-02-13
*
Bug nombres en chiffres décimaux dans les Cases
herbelin
2001-02-12
*
Bug point final dans la syntaxe theorem_body
herbelin
2001-02-09
*
exported a few functions that are used in graphical interface pcoq.
bertot
2001-02-09
*
Several pairs of different functions actually had the same name, so
bertot
2001-02-09
*
modif de la syntax: assoc a droite pour Ring
mayero
2001-02-08
*
Simplifications
herbelin
2001-02-08
*
Modif pour les patterns de sous-termes
delahaye
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Retrait de EvarRef de global_reference; nettoyage autour de ast_of_ref
herbelin
2001-02-07
*
Ajout d'une commande pour afficher chaque coercion à la demande
herbelin
2001-02-06
[next]