aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-01-05Environ: export API to transitively close a set of section variablesEnrico 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-04Future: allow custom action when a delegated future is forcedEnrico Tassi
2014-01-04kernel: save in aux the list of section variables usedEnrico 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
2014-01-04Aux_file: cache information at compile time for later (re)useEnrico Tassi
2014-01-04Remove obsolete comment about Let being processed synchronouslyEnrico Tassi
2014-01-04Code cleaning in Rewrite, may also result faster.Pierre-Marie Pédrot
2014-01-01Reference the 'external' tactic.Guillaume Melquiond
2013-12-30When resetting an evarmap with the unsafe function Evd.evars_reset_evd withPierre-Marie Pédrot
2013-12-30Useless Evd.create_evar_defs.Pierre-Marie Pédrot
2013-12-30Support for evars and metas in native compiler.Maxime Dénès
2013-12-29Avoid generating .ml files in native compiler.Maxime Dénès
2013-12-29Got rid of unused lazy flag in the native compiler.Maxime Dénès
2013-12-28Revert "Partial revert of r16711"Maxime Dénès
2013-12-28Removing native_name reference from constant_body.Maxime Dénès
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-24Future: optional greedy chainingEnrico Tassi
2013-12-24cleanup warningEnrico Tassi
2013-12-24Simplifying the use of hypinfos in Rewrite.Pierre-Marie Pédrot
2013-12-23Rewrite.ml: removing direction flag from hypinfo.Pierre-Marie Pédrot
2013-12-22Do not pass unification flags around in Rewrite.Pierre-Marie Pédrot
2013-12-22Slight code cleaning ensuring more static invariants in Rewrite.Pierre-Marie Pédrot
2013-12-22Adding -bt to coqc.Pierre-Marie Pédrot
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-22Notation variables are now taken into account as possible ltac bound variablesPierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-21Test case for the buggy commutative cut subterm rule.Maxime Dénès
2013-12-20configure.ml: our configure script is now written in ML :-)Pierre Letouzey
2013-12-20Makefile.build: avoid a -ppPierre Letouzey
2013-12-20coqc: execvp is now available even on win32Pierre Letouzey
2013-12-20coqmktop without Unix (simpler all_subdirs)Pierre Letouzey
2013-12-20Remove unused Makefile lines about .elc compilationPierre Letouzey
2013-12-20Warning removalPierre Boutillier
2013-12-20List: Bug 3039 weaker requirement for fold symmetricPierre Boutillier
2013-12-20Coqdep always uses / as dir_sepPierre Boutillier
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Frédéric Besson
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 21:36:06 +0000