aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-24Fix #5763: Strictly positive example is out of order.jkloos
2017-10-20Merge PR #5989: Handle ∞ in coq-makefile timing test-suiteMaxime Dénès
2017-10-20Merge PR #5984: CI: build lambdaRust (which depends on Iris) rather than just...Maxime Dénès
2017-10-20Merge PR #5978: Bugzilla autolink: avoid linking inside links (fix #5974).Maxime Dénès
2017-10-20Merge PR #5972: Fixing link to GitHub issue search, and wording.Maxime Dénès
2017-10-20Merge PR #1155: Use type nonrec in some functor arguments.Maxime Dénès
2017-10-20Merge PR #1147: Remove GeoProof support.Maxime Dénès
2017-10-20Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...Maxime Dénès
2017-10-20Merge PR #1095: [stm] Remove state handling from FuturesMaxime Dénès
2017-10-20Merge PR #960: Uniformize references to BugzillaMaxime Dénès
2017-10-19rename ci-iris-coq -> ci-iris-lambda-rustRalf Jung
2017-10-19Handle ∞ in coq-makefile timing test-suiteJason Gross
2017-10-19Moving bug numbers to BZ# format in the CHANGES file.Théo Zimmermann
2017-10-19Moving bug numbers to BZ# format in the source code.Théo Zimmermann
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-10-19CI: build lambdaRust (which depends on Iris) rather than just IrisRalf Jung
2017-10-18Bugzilla autolink: avoid linking inside links (fix #5974).Gaëtan Gilbert
2017-10-18Merge PR #984: Handling primitive projections in canonical structures.Maxime Dénès
2017-10-18Fixing link to GitHub issue search, and wording.Théo Zimmermann
2017-10-18Merge PR #1149: Moving to GitHub issues.Maxime Dénès
2017-10-18Moving to GitHub issues.Théo Zimmermann
2017-10-17Adding a test for bug BZ#5692.Pierre-Marie Pédrot
2017-10-17unification: fix BZ#5692, recognize prim projs as CS projectionsMatthieu Sozeau
2017-10-17Properly handling projection parameters in canonical structures.Pierre-Marie Pédrot
2017-10-17Handling primitive projections in canonical structures.Pierre-Marie Pédrot
2017-10-17[vernac] [state] Cache freeze/unfreezeEmilio Jesus Gallego Arias
2017-10-17[stm] Remove state-handling from Futures.Emilio Jesus Gallego Arias
2017-10-17[stm] Move interpretation state to VernacentriesEmilio Jesus Gallego Arias
2017-10-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
2017-10-17[stm] First step to move interpretation of Undo commands out of the classifier.Emilio Jesus Gallego Arias
2017-10-16Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`Maxime Dénès
2017-10-16Use type nonrec in some functor arguments.Gaëtan Gilbert
2017-10-16Merge PR #1152: Fix BZ#5785 (make install -j broken)Maxime Dénès
2017-10-15[stdlib] Fix warnings on deprecated `Add Setoid`Emilio Jesus Gallego Arias
2017-10-13Fix some more missing mkdir lines to Makefile.ideJason Gross
2017-10-13Fix BZ#5785 (make install -j broken)Jason Gross
2017-10-13Merge PR #1103: Take Suggest Proof Using outside the kernel.Maxime Dénès
2017-10-12Merge PR #1089: [stm] [toplevel] Move delicate state initialization to the ST...Maxime Dénès
2017-10-12Merge PR #1144: Fix 5776 - `make` gives `ocamlfind: No such file or directory...Maxime Dénès
2017-10-11Remove GeoProof support.Maxime Dénès
2017-10-11Merge PR #1054: Restoring test on ident validity while browsing directory str...Maxime Dénès
2017-10-11Fix 5776 - `make` gives `ocamlfind: No such file or directory` on every execu...Maxime Dénès
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
2017-10-11Merge PR #1143: fix coq_makefile on cygwinMaxime Dénès
2017-10-10Stm.get_hint_ctx: remove unused Str.splitGaëtan Gilbert
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-10Use a nice printer for constant names in Suggest Proof Using.Gaëtan Gilbert
2017-10-10Code factorization Vernacentries.interp on VernacProof.Gaëtan Gilbert
2017-10-10[vernac] Remove "Proof using" hacks from parser.Emilio Jesus Gallego Arias
2017-10-10Take Suggest Proof Using outside the kernel.Gaëtan Gilbert