aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2014-01-14-schedule-vi-checking generates better scriptEnrico Tassi
2014-01-14STM: fix -async-proofs lazyEnrico Tassi
2014-01-13Make Require verbosePierre Boutillier
2014-01-13STM: fix very simple demoEnrico Tassi
2014-01-13Declared ML Module are not uncapitalized/capitalized/uncapitalized/...Pierre Boutillier
2014-01-07typosEnrico Tassi
2014-01-06STM: handle side effects of workers correctlyEnrico Tassi
2014-01-06Algebraized "No such hypothesis" errorsPierre-Marie Pédrot
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05Proof_using: new syntax + suggestionEnrico Tassi
2014-01-05Fix coqc -time (Closes: 3201)Enrico Tassi
2014-01-05STM: fix error messages while in batch mode (closes: 3196)Enrico Tassi
2014-01-05Paral-ITP: cleanup of command line flags and more conservative defaultEnrico Tassi
2014-01-05Fix some warnings with ocamlc 4.01Enrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04Lemmas: export standard proof terminatorEnrico Tassi
2014-01-04Proof_global: Simpler API for proof_terminatorEnrico Tassi
2014-01-04STM: use sec vars in aux file if no Proof using when building .viEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2014-01-04STM: simple refactoringEnrico Tassi
2014-01-04STM: set loc for aux file when interpreting vernacEnrico Tassi
2014-01-04STM: record in aux file proof build and check timeEnrico Tassi
2013-12-30Useless Evd.create_evar_defs.Pierre-Marie Pédrot
2013-12-24STM: capture type checking error (Closes: 3195)Enrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-24CoqIDE: new feedback "incomplete" to signal partial QedEnrico Tassi
2013-12-24cleanup warningEnrico Tassi
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-12-09Fix printing of Ltac's backtrace.Arnaud Spiwack
2013-12-04Stm: remove an assertion.Arnaud Spiwack
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-12-04Vernac classification: allow for commands which start proofs but must be sync...Arnaud Spiwack
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-27Old message Interp returns the state id so that one can BackTo itEnrico Tassi
2013-11-27New option --help-XML-protocol to document the XML procol used by -ideslaveEnrico Tassi
2013-11-27First stab at retrocompatible INTERP messageEnrico Tassi
2013-11-27STM: restart slave after every proofEnrico Tassi
2013-11-25Remove the Hiddentac module.Arnaud Spiwack
2013-11-22Using hashes instead of strings in dynamic tags. In case of collision, anPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 01:02:13 +0000