index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
toplevel
Commit message (
Expand
)
Author
Age
*
First stab at retrocompatible INTERP message
Enrico Tassi
2013-11-27
*
STM: restart slave after every proof
Enrico Tassi
2013-11-27
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
Using hashes instead of strings in dynamic tags. In case of collision, an
Pierre-Marie Pédrot
2013-11-22
*
Do not print tactic notation names at each interpretation step.
ppedrot
2013-11-12
*
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-11-10
*
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-10
*
Revert the previous commit. It broke Coq compilation.
ppedrot
2013-11-09
*
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-09
*
Moving notation types into grammar rule.
ppedrot
2013-11-09
*
Cleaning and documenting Egramcoq.
ppedrot
2013-11-09
*
STM: fix for PG and "Proof term" lines.
gareuselesinge
2013-11-05
*
Fixup bug 3145
pboutill
2013-11-03
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
Made multiple-goal tactic work after all: .
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Fixes parsing of all: followed by a typechecking/evaluation command.
aspiwack
2013-11-02
*
Adds a new goal selector "all:".
aspiwack
2013-11-02
*
Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...
aspiwack
2013-11-02
*
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
aspiwack
2013-11-02
*
Clean up a warning.
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Future: better doc + restore ~pure optimization
gareuselesinge
2013-10-31
*
Conv_orable made functional and part of pre_env
gareuselesinge
2013-10-31
*
Revert the two last commits. My bad, I messed up git-svn commands...
ppedrot
2013-10-29
*
Profile only when CAMLRUNPARAM is set.
ppedrot
2013-10-29
*
Printing heap on every processed sentence.
ppedrot
2013-10-29
*
Removing Evd.undefined_evars.
ppedrot
2013-10-28
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
cList: a few alternative to hashtbl-based uniquize, distinct, subset
letouzey
2013-10-23
*
cList.index is now cList.index_f, same for index0
letouzey
2013-10-23
*
cList: set-as-list functions are now with an explicit comparison
letouzey
2013-10-23
*
Moving potentially costly computation from exception raising to message
ppedrot
2013-10-22
*
STM: proper error message if the GUI edits_at a dummy state
gareuselesinge
2013-10-22
*
STM: do not enrich exceptions more than once
gareuselesinge
2013-10-22
*
STM: send the gui the status of the slaves
gareuselesinge
2013-10-22
*
Coqtop: fix looping over a broken state.
gareuselesinge
2013-10-18
*
declaration_hooks use Ephemeron
gareuselesinge
2013-10-18
*
Future: ported to Ephemeron + exception enhancing
gareuselesinge
2013-10-18
*
STM: not optimize proofs containing an Undo
gareuselesinge
2013-10-18
*
Remove some uses of local modules (some were unused, some were costly).
xclerc
2013-10-14
*
STM: prefix debug messages with slave-id
gareuselesinge
2013-10-11
*
More comments in ide_slave
gareuselesinge
2013-10-11
[next]