aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2013-12-19Using interp_genarg in tactic notations where possible, instead of an ad-hocPierre-Marie Pédrot
2013-12-19test-suite/output/Notations : evar number changePierre Boutillier
2013-12-19Bad use of Obj.magic in interpretation of TacAlias arguments.Pierre Boutillier
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-12-17test guard condition against feature incompatible with prop-extBruno Barras
2013-12-17Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4ePierre Boutillier
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-19 22:23:27 +0000