aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-09-11Merge PR #1032: Make our CI policy clearer and more explicitMaxime Dénès
2017-09-11Disable OSX signing for temporary artifacts.Maxime Dénès
2017-09-11Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`Maxime Dénès
2017-09-11Merge PR #1035: Fix the introduction of SSR refman chapter.Maxime Dénès
2017-09-11Merge PR #1029: Fix a refine anomaly "Evar defined twice".Maxime Dénès
2017-09-11Merge PR #1014: Add option index entry for NativeCompute ProfilingMaxime Dénès
2017-09-11Merge PR #1004: Document primitive projections in more detailMaxime Dénès
2017-09-11Merge PR #987: In Array.smartmap, read and write from same arrayMaxime Dénès
2017-09-11In stm, fixing a typo about flushing debugging messages.Hugo Herbelin
2017-09-11Typo in the header of ide_slave.ml.Hugo Herbelin
2017-09-11Coqide: adding a separating space in some debugging messages.Hugo Herbelin
2017-09-09If backtrace is missing, don't print it.Pierre-Marie Pédrot
2017-09-09Update backtraces only when the Ltac2 Backtrace flag is set.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#26: Ltac1 gives no backtraces.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#18: Terms should show a backtrace when Set Ltac2 Backtrace is set.Pierre-Marie Pédrot
2017-09-09Moving Ltac2 backtraces to the Exninfo mechanism.Pierre-Marie Pédrot
2017-09-09Fix coq/ltac2#25: Control.case should not be able to catch Control.throw.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-29 15:30:25 +0000