aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
2019-06-17[proof] Move declaration hooks to DeclareDef.Emilio Jesus Gallego Arias
2019-06-17[proof] drop parameter from terminator typeEmilio Jesus Gallego Arias
2019-06-17[proof] Unify obligation proof save path: Part I, declareOblEmilio Jesus Gallego Arias
2019-06-17[proofs] Store hooks in the proof object.Emilio Jesus Gallego Arias
2019-06-16Turning "manual_implicits" into a list of position in impargs.ml.Hugo Herbelin
2019-06-16Adding location in warning telling implicit arguments differ in term and type.Hugo Herbelin
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-12Fix #9455: avoid update_global_env when unchanged Global.universes()Gaëtan Gilbert
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-11Fix #10225 (Instance := {} accepts duplicate fields)Gaë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-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ...Gaëtan Gilbert
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
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-04[vernac] Interpret regular vernacs symbolicallyEmilio Jesus Gallego Arias
2019-06-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
2019-06-04Simplify vernacentries calls to classes, remove unused args, reject deprecate...Gaëtan Gilbert
2019-06-04remove leftover commentsEnrico 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-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)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
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaë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-04instance_name grammar entry isn't globalGaëtan Gilbert
2019-06-03Expose set interface to option tablesGaëtan Gilbert
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-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-28Merge PR #10133: mind_kelim is the highest allowed sort instead of a listPierre-Marie Pédrot
2019-05-28Fix #10264: Singleton class field data is erroneous.Pierre-Marie Pédrot
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-26More precise type for Safe_typing export and inlining of private constants.Pierre-Marie Pédrot
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
2019-05-24Remove the indirect opaque accessor hooks from Opaqueproof.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 09:19:02 +0000