aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Restores behaviour of v8.1 for unification problems which fail (backport of 1...Gravatar letouzey2008-11-14
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* Apply vmconv if there are no _undefined_ evars around.Gravatar msozeau2008-11-08
* Slight change of the semantics of user-given casts: they don't reallyGravatar msozeau2008-11-07
* Fix universe problem appearing ConCaT using the existing infrastructure forGravatar msozeau2008-11-07
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Backtrack sur commit 11467 (tentative d'optimisation meta_instance quiGravatar herbelin2008-10-26
* More debugging of handling of open constrs with typeclasses:Gravatar msozeau2008-10-25
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Retour en arrière pour raison de compatibilité sur la suppression du nf_evar Gravatar herbelin2008-10-19
* Optimisation de clenv.ml pour que meta_instance ne soit pas appeléGravatar herbelin2008-10-18
* * Fixed constr_cmp again to handle universes subtyping correctlyGravatar puech2008-10-09
* fixing r11433 again:Gravatar barras2008-10-07
* (Try to) use the conversion oracle also in w_unify to choose which constant toGravatar msozeau2008-10-03
* Fixing constr_cmp, propagating subtyping only right of a productGravatar puech2008-10-02
* Correcting a delta normalization bug in VM (checked by benjamin)Gravatar jforest2008-09-30
* Partial fix for bug #1948: recompute order of dependencies betweenGravatar msozeau2008-09-25
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
* Fix a bug, in fold_constr_with_binders, the types of fixpoints wereGravatar msozeau2008-09-13
* Better handling of the opacity of proof obligations, add the possibility ofGravatar msozeau2008-09-07
* Fix camlp5-ism "Ploc.Exc" and add a unification fix: when solving anGravatar msozeau2008-09-04
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Fix implementation of "Global Instance" which redeclared the sameGravatar msozeau2008-08-27
* Correction de bugs:Gravatar herbelin2008-08-05
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Corrige un bug du commit 11187 (le comportement à respecter étaitGravatar herbelin2008-07-31
* Backport r11289.Gravatar msozeau2008-07-29
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* broke cyclic dependenciesGravatar barras2008-07-24
* A try at allowing matching on applications as a binary syntax node by default.Gravatar msozeau2008-07-22
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Quelques modifications autour du filtrage Ltac:Gravatar herbelin2008-07-16
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* Correction d'un bug dans l'analyse des contraintes non résoluesGravatar herbelin2008-06-29
* Préférence donnée aux constantes qui ne sont pas des projectionsGravatar herbelin2008-06-29
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix bug #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-17 00:14:12 +0000