aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2019-06-13Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLaterEnrico Tassi
2019-06-12Merge PR #10180: `deprecated` attribute support for notations and syntactic d...Théo Zimmermann
2019-06-11Remove the side-effect role from the kernel.Pierre-Marie Pédrot
2019-06-11STM: encode in static types that vernac_when is only used when VtSideffGaëtan Gilbert
2019-06-09[proof] Uniformize Proof_global APIEmilio Jesus Gallego Arias
2019-06-09[save_proof] Make terminator API internal.Emilio Jesus Gallego Arias
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
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 #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
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-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-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico 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[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-04Rename Proof_global.{pstate -> t}Gaëtan Gilbert
2019-06-04Funind: use maybe_open_proof a bit lessGaëtan Gilbert
2019-06-04Alternate syntax for ![]: VERNAC EXTEND Foo STATE proofGaëtan Gilbert
2019-06-04coqpp: add new ![] specifiers for structured proof interactionGaëtan Gilbert
2019-06-04Proof_global: pass only 1 pstate when we don't want the proof stackGaëtan Gilbert
2019-06-04rewrite.ml: remove outdated commentGaëtan Gilbert
2019-06-04rewrite.ml: drop the id returned by new_instance earlierGaëtan Gilbert
2019-06-03Apparently unused ssr nonterminalsJim Fehrle
2019-06-01Allowing Set to be part of universe expressions.Hugo Herbelin
2019-06-01Towards unifying parsing/printing for universe instances and Type's argument.Hugo Herbelin
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27Merge PR #10237: Fix some incorrect uses of proof-local environmentPierre-Marie Pédrot
2019-05-25Documenting syntax "injection ... as [= pat1 ... patn ]".Hugo Herbelin
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Use global env in numeral and string notationsMaxime Dénès
2019-05-24Stop using pstate in global print queriesGaëtan Gilbert
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-23Fixing typos - Part 2JPR
2019-05-22Partly revert micromega parsing using typeclasses.Frédéric Besson
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-21Merge PR #10174: Further cleanup of the side-effect machineryGaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 15:24:02 +0000