aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
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
2008-04-04Protection de rewrite in contre le dépliage des constantes dans w_unify, ce quiherbelin
2008-04-03Essai d'un peu plus de conversion dans apply : suppression de laherbelin
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-04-01Ajout "simple apply" et "simple eapply" pour apply sans unfoldherbelin
2008-04-01Finish enhancemenent of return clause inference from tycons, integratingmsozeau
2008-03-30Modifications diverses et variées :herbelin