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: removing "Termops.compact_named_context_reverse" function
Matej Kosik
2016-08-26
*
|
|
CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...
Matej Kosik
2016-08-26
*
|
|
CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"
Matej Kosik
2016-08-26
*
|
|
Merge remote-tracking branch 'v8.6' into trunk
Matej Kosik
2016-08-25
|
\
|
|
*
|
|
CLEANUP: changing the definition of the "Context.NamedList.Declaration" type
Matej Kosik
2016-08-25
*
|
|
CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...
Matej Kosik
2016-08-25
|
*
|
Do not export an internal function in Namegen.
Pierre-Marie Pédrot
2016-08-25
*
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.get_value" function
Matej Kosik
2016-08-25
*
|
|
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
|
|
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Matej Kosik
2016-08-24
|
|
*
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
|
/
|
/
|
*
|
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-08-17
|
\
|
|
*
Two protections against failures when printing evar_map.
Hugo Herbelin
2016-08-17
|
*
Fixing printing in debugger (no global env in debugger).
Hugo Herbelin
2016-08-17
|
*
Efficiently generate the pretyping contexts.
Pierre-Marie Pédrot
2016-08-16
|
|
\
*
|
|
CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function
Matej Kosik
2016-08-11
*
|
|
CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function
Matej Kosik
2016-08-11
|
*
|
Remove unused optional "predicative" argument.
Guillaume Melquiond
2016-08-10
|
/
/
|
*
Using a dedicated kind of substitutions in evar name generation.
Pierre-Marie Pédrot
2016-08-06
|
*
Using the extended contexts in pretyping.
Pierre-Marie Pédrot
2016-08-05
|
*
Use sets instead of lists for names to avoid in evar generation.
Pierre-Marie Pédrot
2016-08-04
|
*
Simplifying code in evar generation.
Pierre-Marie Pédrot
2016-08-04
|
*
Exporting the renaming API for evar declaration.
Pierre-Marie Pédrot
2016-08-04
|
/
*
Fixing #4906 (regression in printing an error message).
Hugo Herbelin
2016-07-08
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Univ: Use loc even if there are more unbound levels
Matthieu Sozeau
2016-06-29
*
Univs: add source locations of levels
Matthieu Sozeau
2016-06-29
*
Optmimize the subst tactic.
Pierre-Marie Pédrot
2016-06-24
*
Optimize the clear tactic.
Pierre-Marie Pédrot
2016-06-24
*
Optimize the clear tactic.
Pierre-Marie Pédrot
2016-06-24
*
Better algorithm for variable deambiguation in term printing.
Pierre-Marie Pédrot
2016-06-23
*
Document new Hint Mode option.
Matthieu Sozeau
2016-06-16
*
Proofview: extensions for backtracking eauto
Matthieu Sozeau
2016-06-16
*
Implement limited proof search and iterative deepening.
Matthieu Sozeau
2016-06-16
*
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
*
\
Merge remote-tracking branch 'origin/pr/173' into trunk
Enrico Tassi
2016-06-14
|
\
\
|
|
*
Fix a typo in proofs/proofview.mli.
Cyprien Mangin
2016-06-14
|
|
*
Fix usage of Pervasives in goal selectors.
Cyprien Mangin
2016-06-14
|
|
*
Add a comment about the use of a zipper, for clarity.
Cyprien Mangin
2016-06-14
|
|
*
Add a [CList.partitioni] function.
Cyprien Mangin
2016-06-14
|
|
*
Add goal range selectors.
Cyprien Mangin
2016-06-14
|
|
/
|
/
|
*
|
Adding a bit of documentation in the mli.
Pierre-Marie Pédrot
2016-06-09
|
*
STM: proof block detection for bullets and { block }
Enrico Tassi
2016-06-06
|
/
*
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
[prev]
[next]