index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
application patch Claudio
filliatr
2001-05-11
*
Changement de la structure des points fixes
barras
2001-05-03
*
ligne vide lors de l'affichage des messages d'erreur a toplevel entre
barras
2001-04-25
*
Amelioration message args constructeur
herbelin
2001-04-25
*
Messages d'erreur Cases
herbelin
2001-04-24
*
Retire commenatires obsoletes
mohring
2001-04-20
*
un typage sûr pour Goal et Check
filliatr
2001-04-20
*
Cd est silencieux si -silent
filliatr
2001-04-19
*
-boot n'implique plus -batch
filliatr
2001-04-19
*
*** empty log message ***
courant
2001-04-19
*
Reparation du bug de Try
delahaye
2001-04-14
*
Mise en place d'un test de clauses non utilisees
herbelin
2001-04-13
*
Interdiction des 'Save (thm_tok)? id' si thm pas ouvert par Goal
herbelin
2001-04-09
*
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
*
renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocam...
filliatr
2001-04-04
*
Add a Comments command, that does nothing, but is quite useful to to have
bertot
2001-04-04
*
utilisation de Options.if_verbose
filliatr
2001-04-03
*
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
*
option -verbose a coqc; option -i supprimée
filliatr
2001-03-21
*
entetes
filliatr
2001-03-15
*
Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisation
herbelin
2001-03-11
*
protection contre certaines exceptions levees par marshal_{in,out}
barras
2001-03-09
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Typo message Scheme
herbelin
2001-02-28
*
bug Reset et Sections
filliatr
2001-02-28
*
Stringmap -> Idmap
herbelin
2001-02-22
*
ident au lieu de string pour le nom de base de qualid
herbelin
2001-02-16
*
Prise en compte noms longs dans Implicits
herbelin
2001-02-16
*
Erreur sur commit
herbelin
2001-02-14
*
Mise en place d'un système optionnel de discharge immédiat; prise en compte...
herbelin
2001-02-14
*
export a function that is needed in pcoq.
bertot
2001-02-13
*
Make sure the initial state used in a protected loop is the state chose exactly
bertot
2001-02-13
*
Theoreme opaques
mohring
2001-02-12
*
All errors were not well reported before. In particular syntax errors were
bertot
2001-02-10
*
Two pairs of parentheses were missing.
bertot
2001-02-09
*
option -m (utilisation memoire)
filliatr
2001-02-09
*
exported several functions that are used in the graphical interface pcoq.
bertot
2001-02-09
*
changed the design to have command groups executed in a protected manner
bertot
2001-02-09
*
Scratch par defaut si rien n'est specifier dans Add LoadPath
herbelin
2001-02-08
*
Suppression warning no .coqrc
herbelin
2001-02-08
*
export a function that can be used to retrieve the context corresponding
bertot
2001-02-08
*
Meilleure approche du conflit path/freeze/library_root en séquentialisant la...
herbelin
2001-02-07
*
Reparation du pretty-print pour les tactiques
delahaye
2001-02-07
*
Centralisation des add_path dans Mltop a cause de la dependance en add_ml_dir
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 demandeparsing/g_bas...
herbelin
2001-02-06
[next]