index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Turn Pcoq into a regular ML file.
Pierre-Marie Pédrot
2015-10-21
*
Expanding the grammar extensions of Pcoq.
Pierre-Marie Pédrot
2015-10-21
*
Removing the dependencies of Pcoq in IFDEF macros.
Pierre-Marie Pédrot
2015-10-21
*
Expliciting some uses of Compat module.
Pierre-Marie Pédrot
2015-10-21
*
Removing test for bug #3956.
Pierre-Marie Pédrot
2015-10-21
*
Proofview.Goal.sigma returns an indexed evarmap.
Pierre-Marie Pédrot
2015-10-20
*
Indexing Proofview.goals with a stage.
Pierre-Marie Pédrot
2015-10-20
*
Boxing the Goal.enter primitive into a record type.
Pierre-Marie Pédrot
2015-10-20
*
Renaming Goal.enter field into s_enter.
Pierre-Marie Pédrot
2015-10-20
*
Expliciting the uses of the old Tacmach API in Tactics.
Pierre-Marie Pédrot
2015-10-19
*
Removing some unsafe uses of monotonicity.
Pierre-Marie Pédrot
2015-10-19
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-19
|
\
*
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
|
*
Categorizing debug messages as such + NonLogical uses loggers.
Pierre Courtieu
2015-10-19
|
*
Test for #4372 (anomaly in inversion in the presence of fake dependency).
Hugo Herbelin
2015-10-19
*
|
More monotonicity in Tactics.
Pierre-Marie Pédrot
2015-10-19
|
*
Turning anomaly into error for #4372 (weakness of inversion in the
Hugo Herbelin
2015-10-19
*
|
Removing tclEVARS in various places.
Pierre-Marie Pédrot
2015-10-19
*
|
Reducing the uses of tclEVARS in Tactics by using monotonous functions.
Pierre-Marie Pédrot
2015-10-19
*
|
Adding a monotonic variant of Goal.enter and Goal.nf_enter.
Pierre-Marie Pédrot
2015-10-19
*
|
Function debug mode more formatted.
Pierre Courtieu
2015-10-19
|
*
Partly fixes #3225. Removed some old experimental stuff in funind.
Pierre Courtieu
2015-10-19
|
*
Fixed #4274, bad formatting of messages in emacs mode.
Pierre Courtieu
2015-10-19
|
*
Documenting the option "Strict Universe Declaration" in CHANGES.
Pierre-Marie Pédrot
2015-10-19
*
|
Making Evarutil.new_evar monotonous.
Pierre-Marie Pédrot
2015-10-18
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
|
*
Miscellaneous typos, spacing, US spelling in comments or variable names.
Hugo Herbelin
2015-10-18
|
*
Using "__" rather than this unelegant arbitrary "A" for the name of variables...
Hugo Herbelin
2015-10-18
|
*
Reference Manual: Applying standard style recommendation about not
Hugo Herbelin
2015-10-18
|
*
Fixing #4198 (continued): not matching within the inner lambdas/let-ins
Hugo Herbelin
2015-10-18
|
*
Using appropriate lambda decomposition function counting let-ins when
Hugo Herbelin
2015-10-18
|
*
Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,
Hugo Herbelin
2015-10-18
*
|
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
|
*
Lemmas accept the Local flag.
Pierre-Marie Pédrot
2015-10-17
|
*
Test for bug #4325.
Pierre-Marie Pédrot
2015-10-17
|
*
Generalize fix for auto from PMP to eauto and typeclasses eauto.
Matthieu Sozeau
2015-10-16
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-10-16
|
\
|
*
|
Hashcons bytecode generated by the VM.
Pierre-Marie Pédrot
2015-10-16
*
|
Exporting a purely functional interface to bytecode patching.
Pierre-Marie Pédrot
2015-10-16
|
*
Remove left2right reference from the kernel.
Maxime Dénès
2015-10-16
|
*
Merge hint lists instead of appending them. (Fix bug #3199)
Guillaume Melquiond
2015-10-16
|
*
Avoid dependency of the pretyper on C code.
Maxime Dénès
2015-10-15
|
*
Test file for #4346: Set is no longer of type Type
Maxime Dénès
2015-10-15
|
*
Fix #4346 2/2: VM casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
|
*
Fix #4346 1/2: native casts were not inferring universe constraints.
Maxime Dénès
2015-10-15
|
*
Warn user when bytecode compilation fails.
Maxime Dénès
2015-10-15
|
*
Remove now useless exception handler in default conversion.
Maxime Dénès
2015-10-15
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
[next]