aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2017-12-18Merge PR #6380: Add tactics to reset and display the Ltac profileMaxime Dénès
2017-12-18Merge PR #6261: Use \ocaml macro in Extraction chapter; accept OCaml in Extra...Maxime Dénès
2017-12-18Merge PR #6305: Build with windows line endingsMaxime Dénès
2017-12-18[vernac] Cleanup of do_definition.Emilio Jesus Gallego Arias
2017-12-18Merge PR #6217: Do dependencies in 1 command per file class.Maxime Dénès
2017-12-18Removing the FAQ, which has been moved to the GitHub wiki for thisMatt Quinn
2017-12-18Merge PR #6453: [doc] Nit on the manual.Maxime Dénès
2017-12-18Merge PR #6411: Fix #5081 by more fine-grained LtacProf recordingMaxime Dénès
2017-12-18Merge PR #6419: [vernac] Split `command.ml` into separate files.Maxime Dénès
2017-12-18Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.Maxime Dénès
2017-12-17[flags] Make program_mode a parameter for commands in vernac.Emilio Jesus Gallego Arias
2017-12-17[vernac] Split `command.ml` into separate files.Emilio Jesus Gallego Arias
2017-12-17[doc] Nit on the manual.Emilio Jesus Gallego Arias
2017-12-16Fix build fileJim
2017-12-16For bug 6249, Segmentation fault when building Coq on Windows 10.Jim
2017-12-16Let definitions must not contain side-effects when reaching the kernel.Pierre-Marie Pédrot
2017-12-16[make] More build fixes for static plugins and ocamlfind.Emilio Jesus Gallego Arias
2017-12-16[stm] [ide protocol] Allow to include several commands on query.Emilio Jesus Gallego Arias
2017-12-15Overlay for unimath.Gaëtan Gilbert
2017-12-15Do dependencies in 1 command per file class.Gaëtan Gilbert
2017-12-15Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`Maxime Dénès
2017-12-15Merge PR #6431: Compatibility of the Coq macOS package with OS X 10.11.Maxime Dénès
2017-12-15Merge PR #6219: Document undocumented optionsMaxime Dénès
2017-12-15Merge PR #6429: 8.7.1 CHANGES.Maxime Dénès
2017-12-15[econstr] Switch constrintern API to non-imperative style.Emilio Jesus Gallego Arias
2017-12-15Fix #5368: Canonical structure unification fails.Pierre-Marie Pédrot
2017-12-15Compatibility of the Coq macOS package with OS X 10.11.Théo Zimmermann
2017-12-14Pass a ghost location for abstractJason Gross
2017-12-14Make [abstract] nodes show up in the Ltac profileJason Gross
2017-12-14Add documentation for time_constrJason Gross
2017-12-14Deprecate dead option Match Strict (ssr).Gaëtan Gilbert
2017-12-14Deprecate dead code option Congruence Depth.Gaëtan Gilbert
2017-12-14Add named timers to LtacProfJason Gross
2017-12-14Add doc+changelog entries for new LtacProf tacticsJason Gross
2017-12-14Add tactics to reset and display the Ltac profileJason Gross
2017-12-14Merge PR #6386: Catch errors while coercing 'and' intro patternsMaxime Dénès
2017-12-14Merge PR #6116: ssr: fill_occ_pattern: return valid ustate even if no match (...Maxime Dénès
2017-12-14Merge PR #6379: Fix profiling pluginMaxime Dénès
2017-12-14Merge PR #6422: [meta] Minor linking fix.Maxime Dénès
2017-12-14Merge PR #6264: [kernel] Patch allowing to disable VM reduction.Maxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-14Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...Maxime Dénès
2017-12-14Merge PR #6169: Clean up/deprecated optionsMaxime Dénès
2017-12-148.7.1 CHANGES.Théo Zimmermann
2017-12-14Vm_compute: taking into account let-ins in parameters of constructors.Hugo Herbelin
2017-12-14Cosmetic: using "types" rather "constr" in some types of term.mli.Hugo Herbelin
2017-12-14Fixing a bug of Print for inductive types with let-ins in parameters.Hugo Herbelin
2017-12-14Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.Hugo Herbelin
2017-12-14Document Short Module Printing.Gaëtan Gilbert
2017-12-14Document Rewriting Schemes (quickly).Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-25 22:18:57 +0000