aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-05-27[travis] temporary UniMath overlayMaxime Dénès
2017-05-26Merge PR#666: romega revisited : no more normalization trace, cleaned-up reso...Maxime Dénès
2017-05-26Merge PR#655: Extra functions exported in EConstrMaxime Dénès
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-25Merge PR#637: Short cleaning of the interpretation path for constr_with_bindingsMaxime Dénès
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-25Merge PR#406: coq makefile2Maxime Dénès
2017-05-25Merge PR#402: Uniform attribute handling in interfacesMaxime Dénès
2017-05-25[location] [travis] Add overlays for located_switchEmilio Jesus Gallego Arias
2017-05-24[location] Fix warnings.Emilio Jesus Gallego Arias
2017-05-24[location] Renaming "CAst.ast" to "CAst.t"Matej Košík
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24ROmega: division-aware ReflOmegaCore, allowing trace without termsPierre Letouzey
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-24coq_makefile: use -include rather than includeEnrico Tassi
2017-05-24Merge PR#642: Small cleanup on `close_proof` type.Maxime Dénès
2017-05-24Merge PR#650: Fixing an extra bug with pattern_of_constrMaxime Dénès
2017-05-24Merge PR#671: unification.mli: Fix a spelling typo in a commentMaxime Dénès
2017-05-23unification.mli: Fix a spelling typo in a commentJason Gross
2017-05-23add the only targetEnrico Tassi
2017-05-23travis: coq_makefile needs the tipa packageEnrico Tassi
2017-05-23overlay for UniMathEnrico Tassi
2017-05-23coq_makefile: avoid spurious ./ in generated .conf fileEnrico Tassi
2017-05-23Restore 8.5, 8.6 compatibility of STDTIME, TIMECMDJason Gross
2017-05-23coq_makefile: don't quote extra arguments (-arg)Enrico Tassi
2017-05-23Make install a single colon target for retro compatibilityEnrico Tassi
2017-05-23enters coq_makefile2Enrico Tassi
2017-05-23test suite for coq_makefile2Enrico Tassi
2017-05-23coqdep: remove optimization making makefiles harder to writeEnrico Tassi
2017-05-23ocamlfind: coqtop -config prints ocamlfind as found by ./configureEnrico Tassi
2017-05-23coqdep: set FOR_PACK variable for files that need to be packedEnrico Tassi
2017-05-23print_config: print COQ_SRC_SUBDIRSEnrico Tassi
2017-05-23Document --print-version in UsageEnrico Tassi
2017-05-23Put the list of Coq sources subdirectories in one placeEnrico Tassi
2017-05-23Usage.print_config moved to EnvarsEnrico Tassi
2017-05-23CoqProject_file: document in API deprecated featuresEnrico Tassi
2017-05-23CoqProject_file: API and code cleanup (tuples -> records)Enrico Tassi
2017-05-23ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliEnrico Tassi
2017-05-23ide/project_fie.ml4: include standard banner with copyrightEnrico Tassi
2017-05-23test suite for coq_makefileEnrico Tassi
2017-05-23configure: -local set coqdoc destination dir to ./doc rather than ""Enrico Tassi
2017-05-23Bigint.euclid: clarify which sign convention is usedPierre Letouzey
2017-05-23Merge PR#661: Added a test for #4765 (an example of printing abbreviation wit...Maxime Dénès
2017-05-23Merge PR#659: Mention ./configure in INSTALL.docMaxime Dénès
2017-05-23Merge PR#657: [test-suite] Add tests for goal printing.Maxime Dénès
2017-05-23Merge PR#646: Revised behavior on ill-formed identifiersMaxime Dénès
2017-05-23Merge PR#660: Change wrong bullet message.Maxime Dénès
2017-05-23Merge PR#518: Faster universe unificationMaxime Dénès
2017-05-23[vernac] Remove `Save thm id.` command.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 03:07:10 +0000