aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
Commit message (Expand)AuthorAge
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Fixing a regression in unification introduced in r16205 (error raisedGravatar herbelin2013-05-14
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Fixing unfolding of local definitions during unification that appearedGravatar herbelin2013-03-21
* Cosmetic code contraction in evarsolve.ml + test sur unification avec let-in.Gravatar herbelin2013-03-21
* Fix for bug #3004 (thanks Hugo!)Gravatar letouzey2013-03-18
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Repairing r16205: errors raised by check_evar_instance were no longerGravatar herbelin2013-02-28
* A slightly more efficient test of well-typedness of restriction ofGravatar herbelin2013-02-21
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Splitted Evarutil in two filesGravatar ppedrot2013-02-10