aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-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-20Added a test for #4765 (an example of printing abbreviation with binders).Hugo Herbelin
2017-05-20Deprecate -nodoc.Théo Zimmermann
2017-05-20Change wrong bullet message.Théo Zimmermann
2017-05-20Revised behavior on ill-formed identifiers.Hugo Herbelin
2017-05-20Merge PR#276: Stopping injection not to work on discriminable atoms (see #4890).Maxime Dénès
2017-05-20Mention ./configure in INSTALL.docThéo Zimmermann
2017-05-20Merge PR#654: Travis: do not cache opam logs (+prettier spacing)Maxime Dénès
2017-05-20Merge PR#643: [ide] Disable `print_ast` call.Maxime Dénès
2017-05-20Merge PR#474: A fix for #5390 (a useful error on used introduction names was ...Maxime Dénès
2017-05-20[test-suite] Add tests for goal printing.Emilio Jesus Gallego Arias
2017-05-20Merge PR#627: Obligations shrinking: shrink abstraction tooMaxime Dénès
2017-05-20Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Maxime Dénès
2017-05-20Merge PR#648: Allow interactive editing of `plugins/` by adding .dir-locals.elMaxime Dénès
2017-05-20Merge PR#649: Fix a typoMaxime Dénès
2017-05-20Merge PR#651: Re-adding explicit dependency of misc universe test into all_st...Maxime Dénès
2017-05-20Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Maxime Dénès
2017-05-19Travis: do not cache opam logs (+prettier spacing)Gaetan Gilbert
2017-05-19Re-adding explicit dependency of misc universe test into all_stdlib.v.Hugo Herbelin
2017-05-18Fix a typoJason Gross
2017-05-18Add .dir-locals.el to pluginsJason Gross
2017-05-18[toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Emilio Jesus Gallego Arias
2017-05-18[ide] Disable `print_ast` call.Emilio Jesus Gallego Arias