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
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
Syntactic Definition autorisée dans les motifs de Cases (utile notamment
herbelin
2002-04-10
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Correction bug infix sur des varaiables
mohring
2002-03-29
*
Ajout de l'entrée ne_constrarg_list
delahaye
2002-03-19
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
option -dump-glob pour coqdoc
filliatr
2002-02-14
*
substitution et pattern modulo let
barras
2002-02-11
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
changement generation de schema d'elimination, False_rec est primitif, Constr...
mohring
2002-01-31
*
Plusieurs arguments autorisés pour Require et Read Module
herbelin
2002-01-18
*
Bug affichage '++' au lieu de ';'
herbelin
2001-12-21
*
Modif précédente trop violente (cf test-suite/success/CasesDep.v)
herbelin
2001-12-19
*
On ne peut plus appliquer des arguments à une syntaxe primitive
herbelin
2001-12-18
*
affichage correct du type des inductifs et constructeurs en presence
barras
2001-12-18
*
parsing des branches de Cases au niveau lconstr (au lieu de constr)
barras
2001-12-18
*
Ajout syntaxe 'Canonical Structure' en remplacement de @Definition + suppress...
herbelin
2001-12-16
*
MAJ de la traduction en ast des variables de section en qualid
herbelin
2001-12-13
*
compat ocaml 3.03
filliatr
2001-12-13
*
- condition de garde (suite)
barras
2001-12-10
*
nouvel algo de conversion plus uniforme
barras
2001-11-29
*
Retablissement de la commande Existential que j'avais supprime par erreur.
clrenard
2001-11-23
*
types vs constr
herbelin
2001-11-20
*
Diverses petites simplications de la machine de preuves.
clrenard
2001-11-19
*
Re-installation de l'affichage des globaux par des noms courts
herbelin
2001-11-19
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
Prise en compte de la syntaxe [x:=c:t]b comme équivalent de [x:=c::t]b
herbelin
2001-11-08
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Suppression de Logic_Type.sigT, redondant avec Specif.sigT
herbelin
2001-10-24
*
Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR
delahaye
2001-10-23
*
Abstraction de l'immplementation de dirpath et implementation dans l'autre se...
herbelin
2001-10-17
*
Nouvelle correction du bug confusion entre implicites de locaux et de globaux
herbelin
2001-10-15
*
Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...
herbelin
2001-10-12
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Bug collision entre les implicites d'un global et les variables locales de mÃ...
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
*
Ajout de dynamiques pour les quotations constr et tactic
delahaye
2001-10-02
*
Marre des unrecognized objects
herbelin
2001-09-24
*
Réparation des options Set Printing and co
herbelin
2001-09-21
*
Mise en place globalisation optionnelle pour Infix/Distfix
herbelin
2001-09-21
*
Amélioration affichage de print_leaf_entry
herbelin
2001-09-20
*
Rajout 'Set Printing Depth'
herbelin
2001-09-20
*
Transparent
barras
2001-09-20
*
Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles de...
herbelin
2001-09-19
*
Ajout de la profondeur de section à DischargeAt pour gérer l'«open» et le...
herbelin
2001-09-19
*
Search prenait en compte le contenu des sections alors que celui-ci n'existe ...
herbelin
2001-09-14
*
Correction confusion VarNode/SectionVarNode (d'où bug Hints Unfold nom_local)
herbelin
2001-09-14
[next]