index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
engine
Commit message (
Expand
)
Author
Age
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-20
*
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
Normalizing the names of dynamic types to follow a typ_* scheme.
Pierre-Marie Pédrot
2016-05-04
*
Interpretation function can return any untyped value.
Pierre-Marie Pédrot
2016-05-04
*
Removing external uses of Val.inject and making Geninterp.interp return Val.t
Pierre-Marie Pédrot
2016-05-04
*
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
Getting rid of the Geninterp.generic_interp function.
Pierre-Marie Pédrot
2016-05-04
*
Switching to an untyped toplevel representation for Ltac values.
Pierre-Marie Pédrot
2016-05-04
*
Moving Ftactic and Geninterp to the engine folder.
Pierre-Marie Pédrot
2016-05-04
*
Moving Evarutil and Proofview to engine/
Pierre-Marie Pédrot
2016-03-20
*
Making Proofview independent of Logic.
Pierre-Marie Pédrot
2016-03-20
*
Allowing to attach location to universes in UState.
Pierre-Marie Pédrot
2016-02-19
*
merging conflicts with the original "trunk__CLEANUP__Context__2" branch
Matej Kosik
2016-02-15
|
\
*
|
Monotonizing the Evarutil module.
Pierre-Marie Pédrot
2016-02-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-02-13
|
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
|
/
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
*
merge
Matej Kosik
2016-01-11
|
\
|
*
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
Remove some unused functions.
Guillaume Melquiond
2016-01-02
*
|
Remove useless rec flags.
Guillaume Melquiond
2016-01-02
*
|
Remove duplicate declarations.
Guillaume Melquiond
2016-01-01
*
|
Merge branch 'v8.5' into trunk
Guillaume Melquiond
2015-12-31
|
/
*
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
CLEANUP: in the Reduction module
Matej Kosik
2015-12-17
*
API: documenting context_chop and removing a duplicate.
Hugo Herbelin
2015-12-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
*
Fixing compilation of mli documentation.
Hugo Herbelin
2015-12-05
*
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
*
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
Remove unneeded fixpoint in normalize_context_set. Note that it is no
Matthieu Sozeau
2015-12-01
*
More efficient implementation of equality-up-to-universes in Universes.
Pierre-Marie Pédrot
2015-11-26
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
*
More invariants in UState.
Pierre-Marie Pédrot
2015-11-26
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-30
*
Removing some goal unsafeness in inductive schemes.
Pierre-Marie Pédrot
2015-10-29
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-29
*
Removing some unsafe uses of monotonicity.
Pierre-Marie Pédrot
2015-10-19
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
*
Adding a notion of monotonous evarmap.
Pierre-Marie Pédrot
2015-10-18
*
Clarifying and documenting the UState API.
Pierre-Marie Pédrot
2015-10-17
*
Dedicated file for universe unification context manipulation.
Pierre-Marie Pédrot
2015-10-17
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
*
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
[next]