aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Correction de bugs:Gravatar herbelin2008-08-05
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Corrige un bug du commit 11187 (le comportement à respecter étaitGravatar herbelin2008-07-31
* Backport r11289.Gravatar msozeau2008-07-29
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* broke cyclic dependenciesGravatar barras2008-07-24
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* Correction d'un bug dans l'analyse des contraintes non résoluesGravatar herbelin2008-06-29
* Préférence donnée aux constantes qui ne sont pas des projectionsGravatar herbelin2008-06-29
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix bug #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)Gravatar herbelin2008-06-21
* Various improvements in handling of evars in general and typingGravatar msozeau2008-06-21
* Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkGravatar herbelin2008-06-18
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-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
* changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)Gravatar barras2008-06-05
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* fixed bug #1780: a lift was missing (match predicate)Gravatar barras2008-05-29
* Notation concise pour la valeur par défaut des cas reconnus commeGravatar herbelin2008-05-28
* introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...Gravatar barras2008-05-28
* - Correction bug highlighting "Module" dans CoqideGravatar herbelin2008-05-28
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* refined the conversion oracleGravatar barras2008-05-21
* Correction d'un bug de l'unification pattern qui oubliait d'expanserGravatar herbelin2008-05-20
* Better implementation of the set of instances of a given class as a CmapGravatar msozeau2008-05-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 12:45:01 +0000