index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
...
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Corrige un bug du commit 11187 (le comportement à respecter était
herbelin
2008-07-31
*
Backport r11289.
msozeau
2008-07-29
*
Fix bug in term dnet preventing some unifications. Allow "higher-order"
msozeau
2008-07-28
*
Even better test for choosing rewrite or setoid_rewrite.
msozeau
2008-07-26
*
Correction d'une incohérence de typage des inductifs polymorphes: les
herbelin
2008-07-25
*
broke cyclic dependencies
barras
2008-07-24
*
A try at allowing matching on applications as a binary syntax node by default.
msozeau
2008-07-22
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Modification rapide du message d'erreur lorsqu'un _ ne peut être
herbelin
2008-07-18
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Quelques modifications autour du filtrage Ltac:
herbelin
2008-07-16
*
- Improve [Context] vernacular to allow arbitrary binders, not just
msozeau
2008-07-07
*
Fixes in handling of implicit arguments:
msozeau
2008-07-04
*
Various bug fixes in type classes and subtac:
msozeau
2008-07-01
*
Correction d'un bug dans l'analyse des contraintes non résolues
herbelin
2008-06-29
*
Préférence donnée aux constantes qui ne sont pas des projections
herbelin
2008-06-29
*
Code cleanup in typeclasses, remove dead and duplicated code.
msozeau
2008-06-21
*
Fix bug #1889, correct globalization in class declarations.
msozeau
2008-06-21
*
- Implantation de la suggestion 1873 sur discriminate. Au final,
herbelin
2008-06-21
*
Correction bug #1886 (pb unification.ml, report de 11157 de v8.2 vers trunk)
herbelin
2008-06-21
*
Various improvements in handling of evars in general and typing
msozeau
2008-06-21
*
Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk
herbelin
2008-06-18
*
Fix bug in handling of classes and instances inside sections at
msozeau
2008-06-17
*
Better typeclass error messages, always giving the full set of
msozeau
2008-06-17
*
Add possibility to match on defined hypotheses, using brackets to
msozeau
2008-06-16
*
Correction bug 1878 (utilisation de extend_evar déplacée là où une
herbelin
2008-06-14
*
Optionally (and by default) split typeclasses evars into connected
msozeau
2008-06-11
*
Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".
herbelin
2008-06-11
*
- 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-10
*
- Correction de la version simplifiée (filtrage sur deux sig
herbelin
2008-06-09
*
- Documentation de admit et Print Assumptions.
herbelin
2008-06-09
*
- Patch sur "intros until 0"
herbelin
2008-06-08
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
changed w_coerce_to_type to consider remaining unif problems (Hugo\'s patch)
barras
2008-06-05
*
Fixes incorrect handling of existing existentials variables in
msozeau
2008-06-03
*
Improvements on coqdoc by adding more information into .glob
msozeau
2008-05-30
*
fixed bug #1780: a lift was missing (match predicate)
barras
2008-05-29
*
Notation concise pour la valeur par défaut des cas reconnus comme
herbelin
2008-05-28
*
introduced Termops.eq_constr (and constr_cmp) that compares terms up to alpha...
barras
2008-05-28
*
- Correction bug highlighting "Module" dans Coqide
herbelin
2008-05-28
*
- Fix bug #1858, Hint Unfold calling the wrong locate function.
msozeau
2008-05-23
*
refined the conversion oracle
barras
2008-05-21
*
Correction d'un bug de l'unification pattern qui oubliait d'expanser
herbelin
2008-05-20
*
Better implementation of the set of instances of a given class as a Cmap
msozeau
2008-05-15
*
Résolution des problèmes ambigus d'inférence du type de retour des
herbelin
2008-05-14
*
Changement de stratégie vis à vis du commit 10859 sur la gestion des
herbelin
2008-05-12
*
- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait des
herbelin
2008-05-10
*
Mise en place d'un algorithme d'inversion des contraintes de type lors
herbelin
2008-05-05
[prev]
[next]