aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-11-12Do not print tactic notation names at each interpretation step.ppedrot
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Revert the previous commit. It broke Coq compilation.ppedrot
2013-11-09Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-09Moving notation types into grammar rule.ppedrot
2013-11-09Cleaning and documenting Egramcoq.ppedrot
2013-11-05STM: fix for PG and "Proof term" lines.gareuselesinge
2013-11-03Fixup bug 3145pboutill
2013-11-02Adds a tactic give_up.aspiwack
2013-11-02Made multiple-goal tactic work after all: .aspiwack
2013-11-02Adds a shelve tactic.aspiwack
2013-11-02Less use of the list-based interface for goal-bound tactics.aspiwack
2013-11-02Tachmach.New is now in Proofview.Goal.enter style.aspiwack
2013-11-02More Proofview.Goal.enter.aspiwack
2013-11-02Fixes parsing of all: followed by a typechecking/evaluation command.aspiwack
2013-11-02Adds a new goal selector "all:".aspiwack
2013-11-02Replaced monads.ml by an essentially equivalent proofview_gen.ml generated by...aspiwack
2013-11-02Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).aspiwack
2013-11-02Clean up a warning.aspiwack
2013-11-02The tactic [admit] exits with the "unsafe" status.aspiwack
2013-11-02Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.aspiwack
2013-11-02Getting rid of Goal.here, and all the related exceptions and combinators.aspiwack
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-10-31Future: better doc + restore ~pure optimizationgareuselesinge
2013-10-31Conv_orable made functional and part of pre_envgareuselesinge
2013-10-29Revert the two last commits. My bad, I messed up git-svn commands...ppedrot
2013-10-29Profile only when CAMLRUNPARAM is set.ppedrot
2013-10-29Printing heap on every processed sentence.ppedrot
2013-10-28Removing Evd.undefined_evars.ppedrot
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-10-23cList.index is now cList.index_f, same for index0letouzey
2013-10-23cList: set-as-list functions are now with an explicit comparisonletouzey
2013-10-22Moving potentially costly computation from exception raising to messageppedrot
2013-10-22STM: proper error message if the GUI edits_at a dummy stategareuselesinge
2013-10-22STM: do not enrich exceptions more than oncegareuselesinge
2013-10-22STM: send the gui the status of the slavesgareuselesinge
2013-10-18Coqtop: fix looping over a broken state.gareuselesinge
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-10-18Future: ported to Ephemeron + exception enhancinggareuselesinge
2013-10-18STM: not optimize proofs containing an Undogareuselesinge
2013-10-14Remove some uses of local modules (some were unused, some were costly).xclerc
2013-10-11STM: prefix debug messages with slave-idgareuselesinge
2013-10-11More comments in ide_slavegareuselesinge
2013-10-11STM: cancel slaves working on outdated jobsgareuselesinge
2013-10-10STM: a proof with nested proofs cannot be delegatedgareuselesinge
2013-10-10STM: add "Stm Wait" to wait for the slaves to complete their jobsgareuselesinge
2013-10-10Clib: fold_left_until added to CListgareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:19:10 +0000