aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2008-12-31Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->herbelin
2008-12-29- Added support for subterm matching in SearchAbout.herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-26- Extracted from the tactic "now" an experimental tactic "easy" for smallherbelin
2008-12-06Fix exponential behaviour of the typeclasses persistent objects. Droppuech
2008-12-04Fixes for unification and substitution of metas under binders.msozeau
2008-12-03improved simplbarras
2008-12-02Miscellaneous fixes and improvements:herbelin
2008-11-28another bug with simplbarras
2008-11-27Fix (?) a pattern matching compilation problem: msozeau
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
2008-11-27fixing problem with CompCert: reordering resulting from tac change was not cl...barras
2008-11-21fixed problem with r11612barras
2008-11-21fixed exponential behavior of evar unif (ground case)barras
2008-11-14Restores behaviour of v8.1 for unification problems which fail (backport of 1...letouzey
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2008-11-08Apply vmconv if there are no _undefined_ evars around.msozeau
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 06:35:33 +0000