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
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Small cleaning of printing coercion failures in Ltac interpretation.
ppedrot
2013-08-04
*
Removing SortArgType.
ppedrot
2013-07-05
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Adding genarg printer to debugger.
ppedrot
2013-06-19
*
Proof-of-concept: moved four easy-to-handle generic arguments to
ppedrot
2013-06-18
*
Added Genarg as generic argument type.
ppedrot
2013-06-12
*
Uniformizing generic argument types.
ppedrot
2013-06-06
*
Removing useless uses of Gmap.
ppedrot
2013-05-14
*
Robust display of NotConvertibleTypeField errors (fix #3008, #2995)
letouzey
2013-03-21
*
kernel/declarations becomes a pure mli
letouzey
2013-02-26
*
Dir_path --> DirPath
letouzey
2013-02-19
*
use List.rev_map whenever possible
letouzey
2013-02-18
*
New implementation of the conversion test, using normalization by evaluation to
mdenes
2013-01-22
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Modulification of Label
ppedrot
2012-12-18
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Moved Intset and Intmap to Int namespace.
ppedrot
2012-12-14
*
still some more dead code removal
letouzey
2012-10-06
*
Clean-up : no more Proof_type.proof_tree
letouzey
2012-10-06
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Revert "Fixing include printers"
pboutill
2012-08-05
*
Fixing include printers
ppedrot
2012-08-03
*
Bigint: avoid dependency over Pp
letouzey
2012-07-30
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
Split Egrammar into Egramml and Egramcoq
letouzey
2012-05-29
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Debugger vs tracer: Two different behaviors wrt printing: The debugger
herbelin
2012-02-01
*
Revert "New evar_map printer ppevmfull which can typically be installed for"
herbelin
2011-10-17
*
New evar_map printer ppevmfull which can typically be installed for
herbelin
2011-10-17
*
Polishing commits r14492, r14448 and r14407 (tactics propagate
herbelin
2011-09-25
*
Fix unification: detect invalid evar instantiations due to scoping earlier.
msozeau
2011-08-04
*
Finally, pr_goal seems to work for printing v8.2 style goal in debugger.
herbelin
2011-07-16
*
Cleaning debugging printer relative to new proof engine. In
herbelin
2011-06-21
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
Factorize code of rewrite to make way for a new implementation using the
msozeau
2011-02-07
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Print universes in debugging printers
glondu
2010-11-08
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
*
Quick fix for having clenv debug printer working in trunk.
herbelin
2010-06-18
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Added debugging printer for the idmap used at evar definition time for
herbelin
2010-06-12
[next]