index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
ide
/
idetop.ml
Age
Commit message (
Expand
)
Author
2019-06-04
Proof_global: pass only 1 pstate when we don't want the proof stack
Gaëtan Gilbert
2019-05-14
CoqIDE: Treat unknown arguments starting with dash as unknown options rather ...
Hugo Herbelin
2019-05-04
Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.
Pierre-Marie Pédrot
2019-04-29
Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...
Maxime Dénès
2019-04-25
[vernac] [ast] Make location info an attribute of vernaculars.
Emilio Jesus Gallego Arias
2019-04-12
Unify Set and Unset handling for options
Gaëtan Gilbert
2019-04-09
[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.
Emilio Jesus Gallego Arias
2019-04-03
Protect some I/O routines from SIGALRM
Maxime Dénès
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-02-05
[parsing] Use AST node for main parsing entry.
Emilio Jesus Gallego Arias
2019-02-01
[toplevel] Split interactive toplevel and compiler binaries.
Emilio Jesus Gallego Arias
2019-01-27
[ide] fail on unavailable commands before adding to the document
Enrico Tassi
2019-01-24
[STM] explicit handling of parsing states
Enrico Tassi
2018-12-14
[proof] Rework proof interface.
Emilio Jesus Gallego Arias
2018-12-12
Merge PR #9101: Fix 8922 again
Hugo Herbelin
2018-12-10
Treat unmatched goals as new for diffs (highlighted)
Jim Fehrle
2018-12-09
[doc] Enable Warning 50 [incorrect doc comment] and fix comments.
Emilio Jesus Gallego Arias
2018-11-24
[toplevel] Allow to specify default options.
Emilio Jesus Gallego Arias
2018-11-14
Get hyps and goal the same way Printer does; don't omit info
Jim Fehrle
2018-09-20
Current diff code only compares the first current goal of the old and new
Jim Fehrle
2018-08-16
1) Make the diff setting a persistent settting.
Jim Fehrle
2018-07-31
Code to handle "Back" command for diffs.
Jim Fehrle
2018-07-26
Do not set diff printing on by default in CoqIDE.
Pierre-Marie Pédrot
2018-07-23
Displays the differences between successive proof steps in coqtop and CoqIDE.
Jim Fehrle
2018-07-07
Introduce a Pcoq.Entry module for functions that ought to be exported.
Pierre-Marie Pédrot
2018-07-03
Remove unused arguments to Ide_slave.concl_next_tac.
Gaëtan Gilbert
2018-06-18
Remove reference name type.
Maxime Dénès
2018-05-25
Remove some occurrences of Evd.empty
Maxime Dénès
2018-05-21
[ide] Remove special option `-ideslave`
Emilio Jesus Gallego Arias
2018-05-21
[stm] Make toplevels standalone executables.
Emilio Jesus Gallego Arias
