index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Commit message (
Expand
)
Author
Age
*
Making unification of LetIn's expressions more consistent (see #3920).
Hugo Herbelin
2015-01-19
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Univs: Fix alias computation for VMs, computation of normal form of
Matthieu Sozeau
2015-01-17
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Fix issue in printing due to de Bruijn bug when constructing compatibility
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Not "Setting ?n=?p order to ?p:=?n to see if it solves some
Hugo Herbelin
2015-01-12
*
Setting ?n=?p order to ?p:=?n to see if it solves some incompatibilities wrt ...
Hugo Herbelin
2015-01-08
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
Reverting the tentative try to restore the use of second-order
Hugo Herbelin
2015-01-07
*
Propagating the relaxing of filtering started in 48509b6, fixed in
Hugo Herbelin
2015-01-06
*
Fixing old filter bug in second_order_matching.
Hugo Herbelin
2015-01-06
*
Fixing 48509b61 which improved unification as expected but actually
Hugo Herbelin
2015-01-03
*
Tentatively trying to restore the use of second-order typed-based
Hugo Herbelin
2015-01-03
*
Fixing #3895 (thanks to PMP for diagnosis).
Hugo Herbelin
2015-01-03
*
An optimization in the use of unification candidates so as to get the
Hugo Herbelin
2015-01-01
*
Simplifying second_order_matching: no need to invert the linear
Hugo Herbelin
2014-12-30
*
When pretyping [uconstr] closures, don't use the local Ltac variable environm...
Arnaud Spiwack
2014-12-19
*
Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...
Hugo Herbelin
2014-12-19
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Fix for #3154: use CUnix.sys_command to call native compiler.
Maxime Dénès
2014-12-16
*
Tentatively starting to use heuristics for evar-evar resolution: first
Hugo Herbelin
2014-12-15
*
New try on Fixing an evar_map bug revealed by commit 603b66f81 on
Hugo Herbelin
2014-12-15
*
Documenting check_record + changing a possibly undefined int into int option.
Hugo Herbelin
2014-12-15
*
Fix merging of name maps in union of universe contexts.
Matthieu Sozeau
2014-12-14
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
Two fixes in unification (bugs #3782 and #3709)
Matthieu Sozeau
2014-12-12
*
Commit not ready. Sorry.
Hugo Herbelin
2014-12-11
*
Added a CannotSolveConstraint unification error and made experiments
Hugo Herbelin
2014-12-11
*
Fine-tuning unification error (using OccurCheck in evarconv).
Hugo Herbelin
2014-12-11
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Fixing an evar_map bug revealed by commit 603b66f81 on unification flags.
Hugo Herbelin
2014-12-11
*
Fixing orientation of postponed subtyping problems.
Hugo Herbelin
2014-12-10
*
Using a more aggressive test for resolving pattern equations ?n = ?p:
Hugo Herbelin
2014-12-10
*
Setup hook to change the unification algorithm used by evarconv,
Matthieu Sozeau
2014-12-09
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Fixing wrong evar_map in return clause inference, revealed by 48509b611.
Hugo Herbelin
2014-12-08
*
Improved criterion for evar restriction in the configuration
Hugo Herbelin
2014-12-08
*
Improving evar restriction (this is a risky change, as I remember a
Hugo Herbelin
2014-12-07
*
Improved tracking of the origin of evars.
Hugo Herbelin
2014-12-07
*
Had forgotten some debugging printer.
Hugo Herbelin
2014-12-07
*
More consistent printing of evars in evar_map debugging printer.
Hugo Herbelin
2014-12-05
*
Fix debugger Tactic Unification.
Hugo Herbelin
2014-12-05
*
Small cleaning and uniformization in unification flags:
Hugo Herbelin
2014-12-05
*
New approach to deal with evar-evar unification problems in different
Hugo Herbelin
2014-12-04
*
Occur-check in refine.
Arnaud Spiwack
2014-12-04
*
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-12-04
*
In solve_evar_evar, orient the heuristic over arities with different
Hugo Herbelin
2014-12-03
*
When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if
Hugo Herbelin
2014-12-02
[next]