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
*
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
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
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
*
Removing meta_with_name from Evd.
Pierre-Marie Pédrot
2015-09-27
*
Removing subst_defined_metas_evars from Evd.
Pierre-Marie Pédrot
2015-09-27
*
Removing uselessly duplicated function in Evd.
Pierre-Marie Pédrot
2015-09-27
*
Hardening the API of evarmaps.
Pierre-Marie Pédrot
2015-09-26
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
*
Fix documentation.
Matthieu Sozeau
2015-07-27
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
*
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-07-02
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-28
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-01
*
Adding a primitive to the tactic monad to modify the exceptional content.
Pierre-Marie Pédrot
2015-05-07
*
Exposing the minimal amount of internal of the Logic monad in order to
Pierre-Marie Pédrot
2015-05-06
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-23
*
Moving Proofview_monad to the engine/ folder.
Pierre-Marie Pédrot
2015-02-28
*
Adding a new folder corresponding to the low-level part of the pretyper
Pierre-Marie Pédrot
2015-02-27