index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
top_printers.ml
Commit message (
Expand
)
Author
Age
...
*
|
Merging Stdarg and Constrarg.
Pierre-Marie Pédrot
2016-09-21
|
/
*
Fixing extra returns in top_printers.ml (msg_notice not same semantics as pp).
Hugo Herbelin
2016-07-19
*
closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)
Pierre Letouzey
2016-07-03
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-01
|
\
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
*
Pfedit.get_current_context refinement (fix #4523)
Matthieu Sozeau
2016-05-26
*
|
Removing the Entry module now that rules need not be marshalled.
Pierre-Marie Pédrot
2016-05-10
*
|
Moving the Val module to Geninterp.
Pierre-Marie Pédrot
2016-05-04
*
|
Fixing printing of toplevel values.
Pierre-Marie Pédrot
2016-04-08
*
|
Do not export entry_key from Pcoq anymore.
Pierre-Marie Pédrot
2016-03-19
*
|
Simplifying the code of Entry.
Pierre-Marie Pédrot
2016-03-19
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Removing constr generic argument.
Pierre-Marie Pédrot
2016-01-14
*
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
Finer-grained types for toplevel values.
Pierre-Marie Pédrot
2015-12-21
*
|
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
*
|
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
2015-12-18
*
|
Type-safe Egramml.grammar_prod_item.
Pierre-Marie Pédrot
2015-10-27
*
|
Pcoq entries are given a proper module.
Pierre-Marie Pédrot
2015-10-26
|
*
Reverting modifications in dev/top_printers pushed mistakenly.
Pierre-Marie Pédrot
2015-10-14
|
*
Fixing perfomance issue of auto hints induced by universes.
Pierre-Marie Pédrot
2015-10-14
*
|
Splitting kernel universe code in two modules.
Pierre-Marie Pédrot
2015-10-06
*
|
Better debug printers for module paths.
Maxime Dénès
2015-09-20
|
/
*
A printer for printing constants of the env (maybe useful when there are not ...
Hugo Herbelin
2015-07-30
*
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Pierre-Marie Pédrot
2015-02-19
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Update headers.
Maxime Dénès
2015-01-12
*
Compatibility ocaml 3.12.
Hugo Herbelin
2014-12-30
*
More printers for ltac signatures.
Hugo Herbelin
2014-12-16
*
Reactivating option "Set Printing Existential Instances" for asking printing ...
Hugo Herbelin
2014-12-04
*
Adding printers for ppproofview.
Hugo Herbelin
2014-10-13
*
Add debug printers for projections, fix printing of evar constraints
Matthieu Sozeau
2014-10-10
*
Adding printer for named_context_val and Goal.goal in debugger.
Hugo Herbelin
2014-10-09
*
Adding a printer for hints.
Hugo Herbelin
2014-10-07
*
Fixing interpretation of constr under binders which was broken after
Hugo Herbelin
2014-10-02
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Fix debug printing with primitive projections.
Matthieu Sozeau
2014-09-18
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
Debug RAKAM
Pierre Boutillier
2014-08-26
*
- Fix bug #3368, due to wrong use of the Cst_stack for projections.
Matthieu Sozeau
2014-06-11
*
Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...
Matthieu Sozeau
2014-06-10
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Fix issue #88: restrict_universe_context was wrongly forgetting about constra...
Matthieu Sozeau
2014-05-06
*
'Pretty' printer for wf_paths
Pierre
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a debug printer for futures.
Pierre-Marie Pédrot
2014-04-25
[prev]
[next]