aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-06-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...Pierre-Marie Pédrot
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
2019-06-07Merge PR #10330: Dune: run coqc with -w +defaultEmilio Jesus Gallego Arias
2019-06-07Merge PR #10335: simple IO CI branch is now `master`Emilio Jesus Gallego Arias
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...Gaëtan Gilbert
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-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-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-06Remove old overlaysGaëtan Gilbert
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-05Add Andreas Lynge to CREDITSAndreas Lynge
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-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
2019-06-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Rename Proof_global.{t -> stack}Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-28 11:03:57 +0000