aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-03-01Fixing bad comparison in Detyping.Pierre-Marie Pédrot
2014-03-01Useless check when loading notations through import.Pierre-Marie Pédrot
2014-03-01Hunting pervasive equality in native compiler. It seems they were used forPierre-Marie Pédrot
2014-03-01Removing a fishy use of pervasive equality in Ltac backtrace printing.Pierre-Marie Pédrot
2014-02-28Removing Pervasives.compare in Termdn.Pierre-Marie Pédrot
2014-02-28Removing a Pervasives.compare in Term_dnet.Pierre-Marie Pédrot
2014-02-28Pos.compare_cont takes the comparison as first argumentPierre Boutillier
2014-02-28Fix bug 3245: 'simpl nomatch' argument annotation makes cbn go into an infini...Pierre Boutillier
2014-02-28test-suite: opaque term -> opaque proofPierre Boutillier
2014-02-28test-suite: New names for vars but the expected invariant is preservedPierre Boutillier
2014-02-28Fix output test-suite 'simpl tactic' -> 'reduction tactics'Pierre Boutillier
2014-02-28Dead code elimionation in reductionopsPierre Boutillier
2014-02-28.*.aux erased by make distcleanPierre Boutillier
2014-02-28Fix compilation of coq and plugins using coq_makefile under cygwinEnrico Tassi
2014-02-28Fixing a Pervasive.compare.Pierre-Marie Pédrot
2014-02-27Makefile: re-introduce 2 phases to avoid make strange -include'sPierre Letouzey
2014-02-27amending last commitEnrico Tassi
2014-02-27better warningEnrico Tassi
2014-02-27Tacinterp: more refactoring.Arnaud Spiwack
2014-02-27Tacinterp: refactoring using Monad.Arnaud Spiwack
2014-02-27Code refactoring thanks to the new Monad module.Arnaud Spiwack
2014-02-27Remove unsafe code (Obj.magic) in Tacinterp.Arnaud Spiwack
2014-02-27Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Arnaud Spiwack
2014-02-27Get rid of the enterl/glist API for Proofview.Goal.Arnaud Spiwack
2014-02-27Tacinterp: yet another superfluous enterl.Arnaud Spiwack
2014-02-27Tacinterp: spurious enterl.Arnaud Spiwack
2014-02-27Dead code: eval_ltac_constr.Arnaud Spiwack
2014-02-26STM: better debug messagesEnrico Tassi
2014-02-26STM: do not print goals on UndoEnrico Tassi
2014-02-26CoqIDE: print message of "Fail" commandEnrico Tassi
2014-02-26refman: document vi2voEnrico Tassi
2014-02-26STM: better messages when checking/finishing tasksEnrico Tassi
2014-02-26Library: when compiling multiple files, reset the opaque tablesEnrico Tassi
2014-02-26STM: when batch compiling a vo, assert we behave conservativelyEnrico Tassi
2014-02-26coq_makefile: new target vi2voEnrico Tassi
2014-02-26vi2vo: new flag -schedule-vi2voEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26STM: backup/restore remote countersEnrico Tassi
2014-02-26remoteCounter: backup/restoreEnrico Tassi
2014-02-26univ: removing dead codeEnrico Tassi
2014-02-26checker and votour ported to new vo format (after -vi2vo)Enrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-26votour: better error messagesEnrico Tassi
2014-02-26checker: less useless error messagesEnrico Tassi
2014-02-26fix checker w.r.t. mutual_inductive_body and constant_bodyEnrico Tassi
2014-02-26fix checker w.r.t. Dyn.t validationEnrico Tassi
2014-02-26Future: make ~greedy:true the default + new sink commodity APIEnrico Tassi
2014-02-26Future: each computation has a uuidEnrico Tassi
2014-02-25Tacinterp: remove the is_value check in Ltac's let-in.Arnaud Spiwack
2014-02-25Tacinterp: fewer enterl still.Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-02 20:47:15 +0000