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
...
|
*
Refining 0c320e79ba30 in fixing interpretation of constr under binders
Hugo Herbelin
2015-10-11
|
*
Fixing obviously untested fold_glob_constr and iter_glob_constr.
Hugo Herbelin
2015-10-11
|
*
Constr_matching: renaming misleading name stk into ctx.
Hugo Herbelin
2015-10-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
|
*
Fix inference of return clause raising a type error.
Matthieu Sozeau
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Univs: fix bug #3807
Matthieu Sozeau
2015-10-08
|
*
Univs: fix bug #4161.
Matthieu Sozeau
2015-10-08
|
*
Univs: fix FingerTree contrib.
Matthieu Sozeau
2015-10-07
|
*
Univs: add Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-06
|
\
|
|
*
Univs (pretyping): call vm_compute/native_compute with the current
Matthieu Sozeau
2015-10-06
|
*
Fix bug #4354: interpret hints in the right env and sigma.
Matthieu Sozeau
2015-10-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
\
|
|
*
Univs: fix bug #4251, handling of template polymorphic constants.
Matthieu Sozeau
2015-10-02
|
|
*
Univs: fix after rebase (from_ctx/from_env)
Matthieu Sozeau
2015-10-02
|
|
*
Univs: fix many evar_map initializations and leaks.
Matthieu Sozeau
2015-10-02
|
|
*
Univs (pretyping): allow parsing and decl of Top.n
Matthieu Sozeau
2015-10-02
|
|
*
Univs (evd): deal with global universes and sideff
Matthieu Sozeau
2015-10-02
|
|
*
Forcing i > Set for global universes (incomplete)
Matthieu Sozeau
2015-10-02
|
|
*
Univs: force all universes to be >= Set.
Matthieu Sozeau
2015-10-02
|
|
*
Univs: Fix part of bug #4161
Matthieu Sozeau
2015-10-02
|
|
*
Universes: enforce Set <= i for all Type occurrences.
Matthieu Sozeau
2015-10-02
|
|
/
*
|
Removing subst_defined_metas_evars from Evd.
Pierre-Marie Pédrot
2015-09-27
|
*
Fixing loss of extra data in Evd.
Pierre-Marie Pédrot
2015-09-27
*
|
Hardening the API of evarmaps.
Pierre-Marie Pédrot
2015-09-26
|
*
Fixing bug #4347: Not_found Exception with some Records.
Pierre-Marie Pédrot
2015-09-26
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
*
Do not compress match constructs when the inner match contains no branch. (Fi...
Guillaume Melquiond
2015-09-18
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Hugo Herbelin
2015-09-09
|
\
|
|
*
Documenting the code when preference is given to expansion of default
Hugo Herbelin
2015-09-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-05
|
\
|
|
*
Continuing 817308ab (use ltac env for terms in ltac context) + fix
Hugo Herbelin
2015-08-02
|
*
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
|
*
Documenting in passing.
Hugo Herbelin
2015-08-02
|
*
Hopefully clearer printing of stack when debugging evarconv unification.
Hugo Herbelin
2015-08-02
|
*
Cosmetic changes in evarconv.ml: hopefully more regular names and form
Hugo Herbelin
2015-08-02
|
*
Cosmetic changes in evarconv.ml: hopefully more regular form and
Hugo Herbelin
2015-08-02
|
*
Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.
Hugo Herbelin
2015-08-02
|
*
Evarconv.ml: small cut-elimination, saving useless zip.
Hugo Herbelin
2015-08-02
|
*
Cosmetic in evarconv.ml: naming a local function for better readibility.
Hugo Herbelin
2015-08-02
|
*
Fixing #4221 (interpreting bound variables using ltac env was possibly
Hugo Herbelin
2015-08-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-27
|
\
|
|
*
Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.
Pierre-Marie Pédrot
2015-07-21
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
*
Refining 71def2f8 on too strong occur-check limiting evar-evar
Hugo Herbelin
2015-07-16
[prev]
[next]