index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
vernacentries.ml
Commit message (
Expand
)
Author
Age
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...
herbelin
2001-12-16
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
reparation de Locate
barras
2001-11-29
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
Choucroute entre les tables de synchronisation, les options -silent et les et...
letouzey
2001-11-08
*
GROS COMMIT:
barras
2001-11-05
*
Reorganisation de Goption. Passage des options l'utilisant en synchrone
letouzey
2001-10-30
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Amélioration mise en page Print ML Module et Print ML Module
herbelin
2001-10-17
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Réparation des options Set Printing and co
herbelin
2001-09-21
*
Mise en place globalisation optionnelle pour Infix/Distfix
herbelin
2001-09-21
*
Protection contre Not_found
herbelin
2001-09-21
*
Correction bug affichage Infix/Distfix
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
*
Blindage de Show Intro
letouzey
2001-09-17
*
Suppression des library roots, on teste si un nom est absolu autrement
herbelin
2001-09-07
*
Parsing
herbelin
2001-08-10
*
ajout Show Intro(s)
letouzey
2001-07-04
*
Facilites pour le debogguage des univers.
coq
2001-05-29
*
Pretty -> Prettyp
filliatr
2001-05-28
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
*
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
*
Uniformisation des 'Save def_tok id'
herbelin
2001-04-09
*
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
*
entetes
filliatr
2001-03-15
*
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
*
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
*
Theoreme opaques
mohring
2001-02-12
*
Scratch par defaut si rien n'est specifier dans Add LoadPath
herbelin
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
*
Ajout d'une commande pour afficher chaque coercion à la demandeparsing/g_bas...
herbelin
2001-02-06
*
Ajout option Set/Unset/Test Printing Coercions
herbelin
2001-01-31
*
Branchement sur Objdef
herbelin
2001-01-30
*
pas de warning avec Opaque quand is_silent
filliatr
2001-01-29
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
Ajout de constantes locales dans les Records
herbelin
2001-01-24
*
Meta Definition + Tactic Definition
delahaye
2001-01-09
*
Arite cachee de Match Context + Meta Definition
delahaye
2001-01-05
[next]