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
*
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
*
Fixing loss of extra data in Evd.
Pierre-Marie Pédrot
2015-09-27
*
Fixing bug #4347: Not_found Exception with some Records.
Pierre-Marie Pédrot
2015-09-26
*
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
*
Documenting the code when preference is given to expansion of default
Hugo Herbelin
2015-09-08
*
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
*
Fixing bug #4303: Anomaly: Uncaught exception Invalid_argument.
Pierre-Marie Pédrot
2015-07-21
*
Refining 71def2f8 on too strong occur-check limiting evar-evar
Hugo Herbelin
2015-07-16
*
Slight improvement in naming anonymous variables in error messages:
Hugo Herbelin
2015-07-16
*
Fixing #4177 (find_projectable was liable to ask to instantiate an evar twice).
Hugo Herbelin
2015-07-16
*
Fixing bug #4240 (closure_of_filter was not ensuring refinement of
Hugo Herbelin
2015-07-16
*
Fix universe instantiation with canonical structures.
Maxime Dénès
2015-07-16
*
Continuing 93579407, spotting other potential sources of anomaly
Hugo Herbelin
2015-07-16
*
Fixing anomaly #3743 while printing an error message involving evar constraints.
Hugo Herbelin
2015-07-16
*
Continuing handling of NoCoercion after df6e64fd28 and 4944b5e72.
Hugo Herbelin
2015-07-10
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
Make retyping of projections more resilient to wrong environment.
Maxime Dénès
2015-07-09
*
Univs: bug fix.
Matthieu Sozeau
2015-07-07
*
Fix handling of primitive projections in VM.
Maxime Dénès
2015-07-05
*
Assumptions: more informative print for False axiom (Close: #4054)
Enrico Tassi
2015-06-29
*
Fix incompleteness of conversion used by evarconv
Matthieu Sozeau
2015-06-28
*
Fix bug #4254 with the help of J.H. Jourdan
Matthieu Sozeau
2015-06-26
*
Make normalization of primitive projections in native_compute the same as wit...
Maxime Dénès
2015-06-08
*
Fixup for 866c41b
Enrico Tassi
2015-05-28
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Adding an extensible global state to evarmaps.
Pierre-Marie Pédrot
2015-05-19
*
Make Coercion.inh_app_fun respect its specification.
Pierre-Marie Pédrot
2015-05-15
*
Disable precompilation for native_compute by default.
Guillaume Melquiond
2015-05-14
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Fix for a second avatar of bug #4234.
Pierre-Marie Pédrot
2015-05-13
*
Better fixing #4198 such that the term to match is looked for before
Hugo Herbelin
2015-05-13
*
Fixing bug #4234.
Pierre-Marie Pédrot
2015-05-12
[next]