aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Dune: run coqc with -w +defaultGaëtan Gilbert
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain...Pierre-Marie Pédrot
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
2019-06-06Doc for per commit compile lintGaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Merge PR #10323: Remove old overlaysEmilio Jesus Gallego Arias
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
2019-06-06Merge PR #10299: Lazy substitution of section contexts in opaque proofsMaxime Dénès
2019-06-06Fix panel behavior as requested by #10292Claude Stolze
2019-06-06Remove old overlaysGaëtan Gilbert
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
2019-06-05Add Andreas Lynge to CREDITSAndreas Lynge
2019-06-05Remove redundancies in the INSTALL doc.Théo Zimmermann
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-05Add codeowner for Ltac2. Forgotten in #10002.Théo Zimmermann
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-05vernac_load doesn't get a ?proof argumentGaëtan Gilbert
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
2019-06-05Merge PR #10296: Unused ssr ntsEnrico Tassi
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04[vernac] Interpret regular vernacs symbolicallyEmilio Jesus Gallego Arias
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-04Fix typo in changelogEnrico Tassi
2019-06-04Simplify vernacentries calls to classes, remove unused args, reject deprecate...Gaëtan Gilbert
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico Tassi
2019-06-04remove leftover commentsEnrico Tassi
2019-06-04update overlaysEnrico Tassi
2019-06-04[classes] remove program mode from the new_instance_* APIsEnrico Tassi
2019-06-04[vernac] more precise types for Add Morph, Instance, and FunctionEnrico Tassi
2019-06-04[vernac] remove VtMaybeOpenProofEnrico Tassi
2019-06-04[rewrite] Add Morphism syntax made different for module type parametersEnrico Tassi
2019-06-04[function] always open a proof when used with `wf` or `measure`Enrico Tassi
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-04Replace ModifyProofStack by CloseProofGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 00:59:01 +0000