| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
By default, the search command calls `Pp.msg` to print search results.
Unfortunately, this bypasses the `log_via_feedback` option and produces
not very nice results on feedback-depending IDES like JsCoq.
A proper fix would involve merging coq/coq#143 , and the upcoming search
cleanup, but this should do the trick for now.
I couldn't observe any problem with the usual testing.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also:
- fix elim trying to saturate too much and not raising the expected exn
- fix fill_occ_pattern when occ is {-}, it used to lose the
instantiation obtained by matching the term
|
|
|
|
|
|
|
|
|
|
So that Universe Polymorphic constants are compared "correctly",
i.e. not discriminated by the pattern filtering phase (verbatim
head comparison) but eventually by unification.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
