index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
reduction.ml
Commit message (
Expand
)
Author
Age
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
*
Fix checker to handle projections with eta and universe polymorphism correctly.
Matthieu Sozeau
2014-09-06
*
Rename eta_expand_ind_stacks, fix the one from the checker and adapt
Matthieu Sozeau
2014-09-05
*
Fix infer conv using the wrong universe conversion flexibility information
Matthieu Sozeau
2014-08-03
*
Cleanup code for constant equality in kernel conversion.
Matthieu Sozeau
2014-07-21
*
Use kernel conversion on terms that contain universe variables during unifica...
Matthieu Sozeau
2014-07-20
*
In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in M...
Matthieu Sozeau
2014-07-07
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
Moving a Thread.yield in check_interrupt.
Pierre-Marie Pédrot
2014-06-07
*
Adding a new Control file centralizing the control options of Coq.
Pierre-Marie Pédrot
2014-06-07
*
Make kernel reduction code parametric over the handling of universes,
Matthieu Sozeau
2014-06-06
*
- Fix for commit 15999903f875f4b5dbb3d5240d2ca39acc3cd777 which disallowed some
Matthieu Sozeau
2014-05-28
*
- Fix in kernel conversion not folding the universe constraints
Matthieu Sozeau
2014-05-26
*
Update infer_conv to record trivial Prop <= Type i constraints that are neede...
Matthieu Sozeau
2014-05-26
*
- Fix comparison of universes.
Matthieu Sozeau
2014-05-06
*
Restore reasonable performance by not allocating during universe checks,
Matthieu Sozeau
2014-05-06
*
Properly reinstate old-style polymorphism in the kernel and pretyping/retyping.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Paral-ITP: cleanup of command line flags and more conservative default
Enrico Tassi
2014-01-05
*
Support for evars and metas in native compiler.
Maxime Dénès
2013-12-30
*
Tentative fix of the guardedness checker by Christine and me. All stdlib and ...
Matthieu Sozeau
2013-12-17
*
Reduction: every n iterations a slaves process checks for interruption
Enrico Tassi
2013-11-27
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of identifier
ppedrot
2012-12-14
*
Monomorphization (kernel)
ppedrot
2012-11-22
*
More monomorphizations
ppedrot
2012-11-13
*
Monomorphized a lot of equalities over OCaml integers, thanks to
ppedrot
2012-11-08
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Univ: enforce_leq instead of enforce_geq for more uniformity
letouzey
2012-03-22
*
Noise for nothing
pboutill
2012-03-02
*
Propagated information from the reduction tactics to the kernel so
herbelin
2011-08-10
*
Esubst: make types of substitutions & lifts private
puech
2011-08-08
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Starting being more explicit on the reasons why module subtyping fails.
herbelin
2011-03-05
*
Univ.constraints made fully abstract instead of being a Set of abstract stuff
letouzey
2010-12-18
*
Forgotten lifts in eta-expansion
glondu
2010-10-04
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
kernel conversion and reduction do not raise assert failure on ill-typed term...
barras
2010-07-29
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
"Improved" the form of the inferred type of "match" by
herbelin
2010-06-03
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
[next]