aboutsummaryrefslogtreecommitdiff
path: root/vernac
AgeCommit message (Expand)Author
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-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-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
2019-05-23do not parse `|` as infix in patterns; parse `|}` as `|` `}`Georges Gonthier
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ...Maxime Dénès
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
2019-05-22Merge PR #10173: Fail: don't catch critical errorsEmilio Jesus Gallego Arias
2019-05-21[loadpath] Factor in common logic for vio/vo file selection.Emilio Jesus Gallego Arias
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-21Remove definition-not-visible warningGaëtan Gilbert
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
2019-05-20[Classes] Use prepare_parameter from DeclareDef.Emilio Jesus Gallego Arias
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-17Fail: don't catch critical errorsGaëtan Gilbert
2019-05-15Merge PR #10150: Handle tags shorter than "diff." without an exceptionGaëtan Gilbert
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:03:19 +0000