aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau
2008-07-25Correction d'une incohérence de typage des inductifs polymorphes: lesherbelin
2008-07-24broke cyclic dependenciesbarras
2008-07-22A try at allowing matching on applications as a binary syntax node by default.msozeau
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-16Quelques modifications autour du filtrage Ltac:herbelin
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-06-29Correction d'un bug dans l'analyse des contraintes non résoluesherbelin
2008-06-29Préférence donnée aux constantes qui ne sont pas des projectionsherbelin
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-06-21Fix bug #1889, correct globalization in class declarations.msozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-21Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)herbelin
2008-06-21Various improvements in handling of evars in general and typingmsozeau
2008-06-18Propagation des révisions 11144 et 11136 de la 8.2 vers le trunkherbelin
2008-06-17Fix bug in handling of classes and instances inside sections atmsozeau
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
2008-06-11Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".herbelin
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
2008-06-09- Correction de la version simplifiée (filtrage sur deux sigherbelin
2008-06-09- Documentation de admit et Print Assumptions.herbelin
2008-06-08- Patch sur "intros until 0"herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-05changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)barras
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-29fixed bug #1780: a lift was missing (match predicate)barras
2008-05-28Notation concise pour la valeur par défaut des cas reconnus commeherbelin
2008-05-28introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...barras
2008-05-28- Correction bug highlighting "Module" dans Coqideherbelin
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-05-21refined the conversion oraclebarras
2008-05-20Correction d'un bug de l'unification pattern qui oubliait d'expanserherbelin
2008-05-15Better implementation of the set of instances of a given class as a Cmapmsozeau
2008-05-14Résolution des problèmes ambigus d'inférence du type de retour desherbelin
2008-05-12Changement de stratégie vis à vis du commit 10859 sur la gestion desherbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-04-30Réutilisation de l'infrastructure pour le polymorphisme d'univers desherbelin
2008-04-28Backtrack on using metas eagerly in auto, only done in "new auto" formsozeau
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin