aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-27Correction du bug des types singletons pas sous-type de Setherbelin
2008-04-27- Backtrack sur option with_types suite à confusion sur l'utilisationherbelin
2008-04-27- Fix bug in unification not taking into account the right metamsozeau
2008-04-26- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avecherbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-21- Parameterize unification by two sets of transparent_state, one for openmsozeau
2008-04-20Add the ability to give a transparent_state for conversion, tomsozeau
2008-04-18Correction bug 1835 + correction bug occur-check résultant en unherbelin
2008-04-17Bug squashing day !msozeau
2008-04-17Little fixes in setoid_rewrite.msozeau
2008-04-15Mises à jour bugs, CHANGES, code mortherbelin
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Document the new setoid rewrite tactic, and fix a few things whilemsozeau
2008-04-09Fix evar bugs in type classes:msozeau
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin