aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* Really compare evar maps in progress, due to merging in apply and otherGravatar msozeau2009-01-23
* Fixing bug #1918 (no occur-check in Meta unification was done yet!).Gravatar herbelin2009-01-20
* - Fixing bug 1891 (abusive instantiations of evar arguments inGravatar herbelin2009-01-20
* Backporting from v8.2 to trunk:Gravatar herbelin2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Correct a bug in commit 11659Gravatar puech2009-01-16
* Fix a bunch of bugs related to setoid_rewrite, unification and evars:Gravatar msozeau2009-01-12
* Completed 11745 (move of jprover to user contribs) and cleaned 11743Gravatar herbelin2009-01-05
* Fixed bugs #2001 (search_guard was overwriting the guard index givenGravatar herbelin2009-01-04
* Fixed two apparent inconsistencies in matching.ml:Gravatar herbelin2009-01-02
* Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->Gravatar herbelin2008-12-31
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* Fix exponential behaviour of the typeclasses persistent objects. DropGravatar puech2008-12-06
* Fixes for unification and substitution of metas under binders.Gravatar msozeau2008-12-04
* improved simplGravatar barras2008-12-03
* Miscellaneous fixes and improvements:Gravatar herbelin2008-12-02
* another bug with simplGravatar barras2008-11-28
* Fix (?) a pattern matching compilation problem: Gravatar msozeau2008-11-27
* fixed bug 1791: simpl was performing eta expansionGravatar barras2008-11-27
* fixing problem with CompCert: reordering resulting from tac change was not cl...Gravatar barras2008-11-27
* fixed problem with r11612Gravatar barras2008-11-21
* fixed exponential behavior of evar unif (ground case)Gravatar barras2008-11-21
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 10:52:40 +0000