aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-09-08Fix Typo in Doc for `Set Parsing Explicit`staffehn
2017-09-08Normalizing universes before performing term comparison.Pierre-Marie Pédrot
2017-09-08Using EConstr equality check in unification.Pierre-Marie Pédrot
2017-09-08Using a dedicated argument for tactic quotations.Pierre-Marie Pédrot
2017-09-08Fix the introduction of SSR refman chapter.Théo Zimmermann
2017-09-08Parse directly to Sorts.family when appropriate.Gaëtan Gilbert
2017-09-08Move README.ci and link to it from CONTRIBUTING.Théo Zimmermann
2017-09-08Update CI policy.Théo Zimmermann
2017-09-08Fix coq/ltac2#27: ... is not a particularly helpful printing of an error mess...Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#24: There should be a way to turn an exn into a message.Pierre-Marie Pédrot
2017-09-08Fix coq/ltac2#22: Argument to Tactic_failure should be printed.Pierre-Marie Pédrot
2017-09-07Slightly better printing for anonymous closures.Pierre-Marie Pédrot
2017-09-07Fix coq/ltac2#21: Backtraces should print Ltac2 closures.Pierre-Marie Pédrot
2017-09-07Merge PR #997: coqdoc: Support comments in verbatim outputMaxime Dénès
2017-09-07Fix BZ#5655 by avoiding the creation of a cleaner thread for empty queues.Maxime Dénès
2017-09-07Merge PR #1016: 2 Typos in 'Add Parametric Morphism' DocumentationMaxime Dénès
2017-09-07Merge PR #968: Better error messages on the CIMaxime Dénès
2017-09-07dev/build/windows/makecoq_mingw.sh: install camlp5's META fileEnrico Tassi
2017-09-07Merge PR #931: Parametrize module bodyMaxime Dénès
2017-09-07Merge PR #914: Making the detyper lazyMaxime Dénès
2017-09-07Merge PR #904: Add build_coq_or to API.CoqlibMaxime Dénès
2017-09-07Trying to properly propagate errors in Windows CI script.Maxime Dénès
2017-09-07Communicate the backtrace through the monad.Pierre-Marie Pédrot
2017-09-06Fix coq/ltac2#23: Int.compare should not be uniformly 0.Pierre-Marie Pédrot
2017-09-06Using higher-order representation for closures.Pierre-Marie Pédrot
2017-09-06Parameterizing over parameters in ML functions from Tac2core.Pierre-Marie Pédrot
2017-09-06The interp_app function now takes a closure as an argument.Pierre-Marie Pédrot
2017-09-06Moving Tac2ffi before Tac2interp.Pierre-Marie Pédrot
2017-09-06Introducing abstract data representations.Pierre-Marie Pédrot
2017-09-06use get_arguments, String.concat, remove -IPaul Steckler
2017-09-06Fix a refine anomaly "Evar defined twice".Pierre-Marie Pédrot
2017-09-06Code factorization.Pierre-Marie Pédrot
2017-09-06weakens an hypothesis of Rle_RpowerYves Bertot
2017-09-06changed statements of Rpower_lt and Rle_power and addedYves Bertot
2017-09-06Merge PR #1022: Appveyor packageMaxime Dénès
2017-09-05read flags from project file for Compile BufferPaul Steckler
2017-09-05Refine does not evar-normalizes the goal preemptively.Pierre-Marie Pédrot
2017-09-05Make AppVeyor generate Windows package.Maxime Dénès
2017-09-05Binding the firstorder tactic.Pierre-Marie Pédrot
2017-09-05Remove -debug option from Windows build script.Maxime Dénès
2017-09-05Get sources of cygwin packages after building the installer.Maxime Dénès
2017-09-05Adapt Windows build script to new CoqIDE data installation directory.Maxime Dénès
2017-09-05Print more of the Coq build output.Maxime Dénès
2017-09-05Print Coq build output.Maxime Dénès
2017-09-05In regression test mode, run cygwin setup to install dependencies.Maxime Dénès
2017-09-05Export Ltac2.Notations in the Ltac2 entry module.Pierre-Marie Pédrot
2017-09-05The absurd tactic now parses a constr.Pierre-Marie Pédrot
2017-09-05Binding move and intro.Pierre-Marie Pédrot
2017-09-05Merge PR #1011: fix test-suite/coq-makefile/findlib-package on windows after ...Maxime Dénès
2017-09-05Introducing quotations for move locations.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-26 03:10:24 +0000