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
...
*
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
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Ensures that let-in's in arities of inductive types work well. Maybe not
herbelin
2009-08-11
*
pushed evar reduction in kernel
barras
2009-02-06
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
really fixed Georges\' bug
barras
2008-05-15
[prev]
[next]