aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* Résolution des problèmes ambigus d'inférence du type de retour desGravatar herbelin2008-05-14
* Changement de stratégie vis à vis du commit 10859 sur la gestion desGravatar herbelin2008-05-12
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* 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
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* Petites corrections vis à vis des commits 10860, 10859, 10850Gravatar herbelin2008-04-28
* Quelques bricoles autour de l'unification:Gravatar herbelin2008-04-27
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* - Backtrack sur option with_types suite à confusion sur l'utilisationGravatar herbelin2008-04-27
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* - Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecGravatar herbelin2008-04-26
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Parameterize unification by two sets of transparent_state, one for openGravatar msozeau2008-04-21
* Add the ability to give a transparent_state for conversion, toGravatar msozeau2008-04-20
* Correction bug 1835 + correction bug occur-check résultant en unGravatar herbelin2008-04-18
* Bug squashing day !Gravatar msozeau2008-04-17
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* Mises à jour bugs, CHANGES, code mortGravatar herbelin2008-04-15