index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
Commit message (
Expand
)
Author
Age
*
No need anymore to refer to COQLIB in ocamldebug-coq
letouzey
2012-08-23
*
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
*
Severe reorganisation of the code of tactics in Proofview.
aspiwack
2012-07-11
*
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
*
Some documentation of recent changes concerning interfaces
letouzey
2012-05-29
*
place all pretty-printing files in new dir printing/
letouzey
2012-05-29
*
Extend become a mli-only file in intf/
letouzey
2012-05-29
*
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
*
Strongly reduce the dependencies of grammar.cma, modulo two hacks
letouzey
2012-05-29
*
Pattern as a mli-only file, operations in Patternops
letouzey
2012-05-29
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Tacexpr as a mli-only, the few functions there are now in Tacops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Vernacexpr is now a mli-only file, locality stuff now in locality.ml
letouzey
2012-05-29
*
Coqide MacOS integration refresh
pboutill
2012-04-27
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
Removing Dhyp from debugger.
herbelin
2012-04-06
*
Everything compiles again.
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
Debugger vs tracer: Two different behaviors wrt printing: The debugger
herbelin
2012-02-01
*
Added new command "Set Parsing Explicit" for deactivating parsing (and
herbelin
2012-01-20
*
Suspending declaration of undefined debug printers.
herbelin
2011-12-18
*
Renamig support added to "Arguments"
gareuselesinge
2011-11-21
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
First attempt at making Print Assumption compatible with opaque modules (fix ...
letouzey
2011-10-25
*
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
*
dev/base_include: display a nice message at the end of the load
letouzey
2011-10-15
*
debugging.txt: no more typing of #use "include" if using .ocamlinit
letouzey
2011-10-15
*
Moved to a more standard order of arguments (i.e. env followed by evar_map)
herbelin
2011-10-11
*
Moving never-used comments from Zhints.v to dev/doc so as not to
herbelin
2011-10-01
*
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
*
Add printer dependency to Hashtbl_alt (used in Term)
puech
2011-07-29
*
Fixed a "feature" of "inversion" and "dependent rewrite" revealed by
herbelin
2011-07-18
*
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 few comments and a dev file to summarize issues with unification
herbelin
2011-06-13
*
A new mechanism to handle errors.
aspiwack
2011-05-13
*
As many notation for for vectors as for List.
pboutill
2011-05-03
*
dev/base_include: no more mod_self_id
letouzey
2011-04-26
*
- Remove create_evar_defs
msozeau
2011-04-13
*
Fix dev/base_include after change of constant_body
letouzey
2011-04-06
*
Adapt printers.mllib after my last commit
letouzey
2011-03-16
*
Annotations at functor applications:
letouzey
2011-02-11
[next]