aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2004-07-11Backtrack sur l'eta-expansion systematique et incorrect du predicat du Cases ...herbelin
2004-07-09majfilliatr
2004-07-08majfilliatr
2004-07-08majfilliatr
2004-07-08* <style>...</style> tag no longer generated for theory filessacerdot
2004-07-08- recent changes to doubleTypeInference.ml (that introduced doublesacerdot
2004-07-08Commit to perform double type inference also on inner types.sacerdot
2004-07-08added commands to idecorbinea
2004-07-07majfilliatr
2004-07-07bypass w_Define when w_refine-ingcorbinea
2004-07-06majfilliatr
2004-07-05majfilliatr
2004-07-05Constants just after a "Let id : t. ... Qed" local variable declaration weresacerdot
2004-07-04majfilliatr
2004-07-02majfilliatr
2004-07-02syntax compatibility fixcorbinea
2004-07-01majfilliatr
2004-06-30majfilliatr
2004-06-30majfilliatr
2004-06-30updated printing of evar context (may loop ?)corbinea
2004-06-30instantiate entry: constr -> lconstrcorbinea
2004-06-29majfilliatr
2004-06-29majfilliatr
2004-06-29Essai de suppression de eta dans simpl (cf bug #779)herbelin
2004-06-29moved instantiate binding to extratacticscorbinea
2004-06-29License de contrib/interfaceherbelin
2004-06-29efficacite du lexeurfilliatr
2004-06-28majfilliatr
2004-06-28majfilliatr
2004-06-28contrib/interface *$*$@!corbinea
2004-06-28more evar stuffcorbinea
2004-06-28Ajout de la coercion id dans context vers evaluable constant (bug #777)herbelin
2004-06-28Correction bug #776herbelin
2004-06-28Double bug d'affichage des cases dépendants (bug #784)herbelin
2004-06-28Modules et Records: gros changements pour prendre en compte le nouveau mind_r...letouzey
2004-06-27majfilliatr
2004-06-27majfilliatr
2004-06-27Typo (bug #797)herbelin
2004-06-27Correction affichage v8 des records avec let (bug #798)herbelin
2004-06-26Licence changed from GPL to Lesser GPL.sacerdot
2004-06-26effective evar refiningcorbinea
2004-06-25majfilliatr
2004-06-25eq and eqT are the samebarras
2004-06-25simplified proof (eq and eqT are now the same)barras
2004-06-25correspondance des records et noms de champs de records entre un module et sa...letouzey
2004-06-24majfilliatr
2004-06-23majfilliatr
2004-06-22majfilliatr
2004-06-21majfilliatr
2004-06-20majfilliatr