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
*
Another bug (de Bruijn) in continuing cf6a68b45 and d64b5766a on
Hugo Herbelin
2015-02-24
*
Compensating 6fd763431 on postponing subtyping evar-evar problems.
Hugo Herbelin
2015-02-23
*
Fixing cf6a68b45 on integrating ensure_evar_independent into is_constrainable...
Hugo Herbelin
2015-02-23
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Fixing rewrite/subst when the subterm to rewrite is argument of an Evar.
Hugo Herbelin
2015-02-23
*
Fixing occur-check which was too strong in unification.ml.
Hugo Herbelin
2015-02-23
*
Fixing bug #3071.
Pierre-Marie Pédrot
2015-02-21
*
Continuing experimentation on what part of the instance of an evar
Hugo Herbelin
2015-02-21
*
Removing need for ensure_evar_independent by passing a force flag to is_const...
Hugo Herbelin
2015-02-21
*
When looking for restrictions in ?n=?p problems, keep the type of let-bindings.
Hugo Herbelin
2015-02-19
*
Remove some dead code and add test-suite file.
Matthieu Sozeau
2015-02-16
*
Fix bug #3960: potential evar instance categorized as an unresolvable
Matthieu Sozeau
2015-02-16
*
Fix 'don't expose cases' in cbn
Pierre Boutillier
2015-02-15
*
Fixing bug #3490.
Pierre-Marie Pédrot
2015-02-15
*
Fixing bug #3916.
Pierre-Marie Pédrot
2015-02-15
*
Univs: fix bug #3755. We were missing refreshements of universes in
Matthieu Sozeau
2015-02-14
*
Fixing #3997 (occur-check in the presence of primitive projections, patch
Hugo Herbelin
2015-02-12
*
Fixing bug #3900.
Pierre-Marie Pédrot
2015-02-11
*
Fixing #4001 (missing type constraints when building return clause of match).
Hugo Herbelin
2015-02-10
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
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
[next]