aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Expand)AuthorAge
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Update CHANGES and INSTALLGravatar glondu2008-09-07
* Renaming parser -> coq-parserGravatar glondu2008-08-18
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Add -browser option to configure scriptGravatar glondu2008-07-27
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* - Suppression de Rstar/Newman peu utilisables comme biblio (encodageGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* MAJ fichiers spécifiques trunkGravatar herbelin2008-06-22
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* MAJ diversesGravatar herbelin2008-06-11
* Documentation de "instantiate".Gravatar glondu2008-06-09
* - Documentation de admit et Print Assumptions.Gravatar herbelin2008-06-09
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* add tiny change to coqideGravatar jnarboux2008-06-07
* One (last?) more update of CHANGES.Gravatar letouzey2008-06-05
* more updates of CHANGESGravatar letouzey2008-06-04
* Some updates of CHANGES (to be continued...)Gravatar letouzey2008-06-03
* Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided inGravatar letouzey2008-06-01
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
* update changes related to coqideGravatar jnarboux2008-05-27
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* Ajout de la possibilité d'utiliser fix/cofix dans les notations.Gravatar herbelin2008-05-24
* refined the conversion oracleGravatar barras2008-05-21
* Léger backtrack sur commit coqide précédent (si la commande à annulerGravatar herbelin2008-05-20
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
* MAJ et bricoles diversesGravatar herbelin2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]Gravatar herbelin2008-05-09
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Réutilisation de l'infrastructure pour le polymorphisme d'univers desGravatar herbelin2008-04-30
* Ajout notation [ x ; ... ; y ] dans list_scope. Changement de laGravatar herbelin2008-04-29
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Change default eauto depth to 100 in setoid_rewrite, bump necessaryGravatar msozeau2008-04-23
* Bug squashing day !Gravatar msozeau2008-04-17
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Suite 10760Gravatar herbelin2008-04-05
* Mise en place d'une extension de apply pour que celui-ci sacheGravatar herbelin2008-04-04
* Quelques améliorations des intro patterns:Gravatar herbelin2008-04-04
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01