index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
/
coqtop.ml
Commit message (
Expand
)
Author
Age
*
Moving the typing_flags to the environment.
Pierre-Marie Pédrot
2016-06-18
*
--print-version produces machine readable version info
Enrico Tassi
2016-06-16
*
Merge remote-tracking branch 'origin/pr/166' into trunk
Enrico Tassi
2016-06-14
|
\
*
\
Merge remote-tracking branch 'origin/pr/182' into trunk
Enrico Tassi
2016-06-14
|
\
\
*
\
\
Merge remote-tracking branch 'origin/pr/173' into trunk
Enrico Tassi
2016-06-14
|
\
\
\
*
|
|
|
Moving back Ltac profiling to the Ltac folder.
Pierre-Marie Pédrot
2016-06-14
|
*
|
|
STM: each proof block can be enabled separately
Enrico Tassi
2016-06-06
|
*
|
|
STM: proof block detection made optional + simple test
Enrico Tassi
2016-06-06
*
|
|
|
-profileltac -> -profile-ltac, as per @herbelin
Jason Gross
2016-06-05
*
|
|
|
LtacProf for Coq trunk
Jason Gross
2016-06-05
|
/
/
/
|
*
|
STM delegation policy can be customized
Enrico Tassi
2016-05-31
*
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
/
/
|
*
coqc: support -o option to specify output file name
Enrico Tassi
2016-05-19
|
/
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-09
|
\
|
*
Rename Lexer -> CLexer.
Pierre-Marie Pédrot
2016-05-09
*
|
Removing dead code and unused opens.
Pierre-Marie Pédrot
2016-05-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
*
Fix bug #4705: coqtop accepts both -emacs and -ideslave.
Pierre-Marie Pédrot
2016-05-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-29
|
\
|
|
*
Restore warnings produced by the interpretation of the command line
Hugo Herbelin
2016-01-22
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
|
*
Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.
Maxime Dénès
2016-01-15
*
|
Remove deprecated command-line options such as "-as".
Guillaume Melquiond
2016-01-06
*
|
CLEANUP: simplifying "Coqtop.init_gc" implementation
Matej Kosik
2015-12-18
*
|
CLEANUP: removing unnecessary wrapper function
Matej Kosik
2015-12-18
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-15
|
\
|
|
*
Flag -compat 8.4 now loads Coq.Compat.Coq84.
Maxime Dénès
2015-12-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-15
|
\
|
|
*
Remove -vm flag of coqtop.
Maxime Dénès
2015-10-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-10
|
\
|
|
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
Spawn: use each socket exclusively for writing or reading
Enrico Tassi
2015-10-08
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
*
Prevent States.intern_state and System.extern_intern from looking up files in...
Guillaume Melquiond
2015-09-29
|
*
Remove some uses of Loadpath.get_paths.
Guillaume Melquiond
2015-09-29
|
*
Make -load-vernac-object respect the loadpath.
Guillaume Melquiond
2015-09-28
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-25
|
\
|
|
*
The -require option now accepts a logical path instead of a physical one.
Pierre-Marie Pédrot
2015-09-25
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-05
|
\
|
|
*
For convenience, making yes and on, and no and off synonymous in
Hugo Herbelin
2015-08-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
|
*
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-25
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-24
|
\
|
|
*
when OCAML_GC_STATS points to a filepath, write Gc stats into it
Gabriel Scherer
2015-06-24
*
|
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-23
|
*
Warning are enabled by default in interactive mode.
Pierre-Marie Pédrot
2015-06-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-01
|
\
|
[next]