aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-10-23Point HoTT back at master, which now supports Coq masterJason Gross
2017-10-18Merge PR #984: Handling primitive projections in canonical structures.Maxime Dénès
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-16Merge PR #1153: [stdlib] Fix warnings on deprecated `Add Setoid`Maxime Dénès
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-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
2017-10-10Merge PR #1140: Fix Travis OSX deploy conditional.Maxime Dénès
2017-10-10Fix BZ#5780: coq_makefile broken under CygwinRalf Jung
2017-10-10Merge PR #540: [configure] Support for flambda flags.Maxime Dénès
2017-10-10Merge PR #1116: Updating citing Coq in FAQ.Maxime Dénès
2017-10-10Updating citing Coq in FAQ.Hugo Herbelin
2017-10-10Restoring test on ident validity while browsing directory structure.Hugo Herbelin
2017-10-10Adding headers to segmenttree.{ml,mli}.Hugo Herbelin
2017-10-10Merge PR #1137: Include leading zeros in version infoMaxime Dénès
2017-10-10Merge PR #768: Omega and romega know about context definitions (fix old bug 148)Maxime Dénès
2017-10-10Merge PR #1053: [deps] Move `Discharge` to `interp`Maxime Dénès
2017-10-10Merge PR #1067: Iris CI: use opam to install dependenciesMaxime Dénès
2017-10-10[flambda] [native] Pass `-Oclassic` to the native compiler.Emilio Jesus Gallego Arias
2017-10-10[configure] Support for flambda flags.Emilio Jesus Gallego Arias
2017-10-09Merge PR #1087: [stm] Switch to a functional APIMaxime Dénès
2017-10-09Merge PR #1126: [ltac] Warning for deprecated `Add Setoid` and `Add Morphism`...Maxime Dénès
2017-10-09Merge PR #1134: Revert "Switch Travis to OSX 10.12 and Xcode 8.3.3."Maxime Dénès
2017-10-09Merge PR #1133: Fix hardcoded boot dependencies after #1041.Maxime Dénès
2017-10-09Merge PR #1132: TimeFileMaker.py: Allow trailing spacesMaxime Dénès
2017-10-09Merge PR #1115: Autolink to Github PRs from BugzillaMaxime Dénès
2017-10-09Merge PR #1114: Generic handling of nameable objects for pluginsMaxime Dénès
2017-10-09Merge PR #1109: Handle some misc todosMaxime Dénès
2017-10-09[deps] Move `Discharge` to `interp`Emilio Jesus Gallego Arias
2017-10-09Merge PR #1086: [stm] [flags] Move document mode flags to the STM.Maxime Dénès
2017-10-09Merge PR #1062: BZ#5739, Allow level for leftmost nonterminal for printing-on...Maxime Dénès