aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaë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-04instance_name grammar entry isn't globalGaëtan Gilbert
2019-06-04rewrite.ml: drop the id returned by new_instance earlierGaëtan Gilbert
2019-06-03Merge PR #10287: Update tutorial plugin to use sigma instad of evd, in keepin...Enrico Tassi
2019-06-03Merge PR #10280: Fixed typo in CONTRIBUTING.mdThéo Zimmermann
2019-06-03Merge PR #10277: Remove Show Script (deprecated in 8.10)Théo Zimmermann
2019-06-03Merge PR #10261: Update doc to reflect that PG now supports Coq-generated pro...Théo Zimmermann
2019-06-03Fix affiliation and ordering in CREDITSTalia Ringer
2019-06-03Update tutorial plugin to use sigma, in keeping with doc recommendationsTalia Ringer
2019-06-03Update doc to reflect that PG now supports Coq-generated proof diffsJim Fehrle
2019-05-31Fixed typo in CONTRIBUTING.mdJose Fernando Lopez Fernandez
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-30Merge PR #10269: Checker: don't use monomorphic universes attached to a constantPierre-Marie Pédrot
2019-05-29Merge PR #10252: Various dynamic assertions and cleanups in opaque typingMaxime Dénès
2019-05-29Merge PR #10248: Move the Discharge module in the kernel and merge it with Co...Maxime Dénès
2019-05-29Merge PR #10270: Fix debug printersEnrico Tassi
2019-05-29Merge PR #10049: [elaboration] Bidirectionality hintsEnrico Tassi
2019-05-28Merge PR #10228: gitlab: run less jobs unless FULL_CI=trueEmilio Jesus Gallego Arias
2019-05-28Fix printers.sh test when missing coqtop.byte, print more infoGaëtan Gilbert
2019-05-28Merge PR #10258: Remove the delayed universe table from object files.Enrico Tassi
2019-05-28Fix [Drop. #use "include";;] for indirect_accessorGaëtan Gilbert
2019-05-28[elaboration] Bidirectionality hintsMaxime Dénès
2019-05-28Same universe constraint fix for the checker.Pierre-Marie Pédrot
2019-05-28Checker: don't use monomorphic universes attached to a constantGaëtan Gilbert
2019-05-28Merge PR #10133: mind_kelim is the highest allowed sort instead of a listPierre-Marie Pédrot
2019-05-27Remove the delayed universe table from object files.Pierre-Marie Pédrot
2019-05-27Merge PR #10249: More precise type for export and inlining of private constantsMaxime Dénès
2019-05-27Fix #10251: Type-checking of polymorphic opaque constr entry types is broken.Pierre-Marie Pédrot
2019-05-27Specific code path for opaque polymorphic constants.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that non-opaque definitions are always side-effect free.Pierre-Marie Pédrot
2019-05-27Ensure dynamically that opaque definitions come with their type.Pierre-Marie Pédrot
2019-05-27gitlab: run less jobs unless FULL_CI=trueGaëtan Gilbert
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-27Merge PR #10241: Update README.md / add SUPPORT.md file.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-06 10:29:09 +0000