aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-11-07Fix universe problem appearing ConCaT using the existing infrastructure formsozeau
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-26Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiherbelin
2008-10-25More debugging of handling of open constrs with typeclasses:msozeau
2008-10-23Open notation for declaring record instances.msozeau
2008-10-19Retour en arrière pour raison de compatibilité sur la suppression du nf_evar herbelin
2008-10-18Optimisation de clenv.ml pour que meta_instance ne soit pas appeléherbelin
2008-10-09* Fixed constr_cmp again to handle universes subtyping correctlypuech
2008-10-07fixing r11433 again:barras
2008-10-03(Try to) use the conversion oracle also in w_unify to choose which constant tomsozeau
2008-10-02Fixing constr_cmp, propagating subtyping only right of a productpuech
2008-09-30Correcting a delta normalization bug in VM (checked by benjamin)jforest
2008-09-25Partial fix for bug #1948: recompute order of dependencies betweenmsozeau
2008-09-15Fix bug #1943 and restrict the inference optimisation of Program tomsozeau
2008-09-14Fix bug #1936: uncaught exception due to undefinable exceptions.msozeau
2008-09-14Fix bug #1940: uncaught exception when searching for a type class.msozeau
2008-09-13Fix a bug, in fold_constr_with_binders, the types of fixpoints weremsozeau
2008-09-07Better handling of the opacity of proof obligations, add the possibility ofmsozeau
2008-09-04Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anmsozeau
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-27Fix implementation of "Global Instance" which redeclared the samemsozeau
2008-08-05Correction de bugs:herbelin
2008-08-05Correction bug de filtrage sous-terme #1920 introduit dans commitherbelin
2008-08-05Suite 11187 et 11298 : ne retarder le dépliage d'une projectionherbelin
2008-08-04Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-31Corrige un bug du commit 11187 (le comportement à respecter étaitherbelin
2008-07-29Backport r11289.msozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 03:53:23 +0000