aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
The main idea of this PR is to distinguish the types of "proof object" `Proof_global.t` and the type of "proof object associated to a constant, the new `Lemmas.t`. This way, we can move the terminator setup to the higher layer in `vernac`, which is the one that really knows about constants, paving the way for further simplification and in particular for a unified handling of constant saving by removal of the control inversion here. Terminators are now internal to `Lemmas`, as it is the only part of the code applying them. As a consequence, proof nesting is now handled by `Lemmas`, and `Proof_global.t` is just a single `Proof.t` plus some environmental meta-data. We are also enable considerable simplification in a future PR, as this patch makes `Proof.t` and `Proof_global.t` essentially the same, so we should expect to handle them under a unified interface.
2019-06-09Merge PR #8726: More robust treatment of the Discharge statusPierre-Marie Pédrot
Reviewed-by: aspiwack Ack-by: ejgallego Reviewed-by: ppedrot
2019-06-09Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint jobEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-06-08Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.Hugo Herbelin
2019-06-08Cleaning the status of Local Definition and similar.Hugo Herbelin
Formerly, knowing if a declaration was to be discharged, to be global but invisible at import, or to be global but visible at import was obtained by combining the parser-level information (i.e. use of Variable/Hypothesis/Let vs use of Axiom/Parameter/Definition/..., use of Local vs Global) with the result of testing whether there were open sections. We change the meaning of the Discharge flag: it does not tell anymore that it was syntactically a Variable/Hypothesis/Let, but tells the expected semantics of the declaration (issuing a warning in the parser-to-interpreter step if the semantics is not the one suggested by the syntax). In particular, the interpretation/command engine becomes independent of the parser. The new "semantic" type is: type import_status = ImportDefaultBehavior | ImportNeedQualified type locality = Discharge | Global of import_status In the process, we found a couple of inconsistencies in the treatment of the locality status. See bug #8722 and test file LocalDefinition.v.
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: ejgallego
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Remove old overlaysGaëtan Gilbert
I updated the readme example using the most recent overlay with only 1 touched development.
2019-06-06Merge PR #8988: Towards unifying parsing/printing for universe instances and ↵Gaëtan Gilbert
Type's argument Reviewed-by: SkySkimmer Reviewed-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-06-04update overlaysEnrico Tassi
2019-06-04VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)Gaëtan Gilbert
+ hide interp_functional_vernac in vernacentries
2019-06-04Overlays for coq/coq#10050 (proof_global API changes)Gaëtan Gilbert
2019-06-04Vernacextend only returns a proof_global.t option, not a vernacstateGaëtan Gilbert
2019-06-01Adding overlay for elpiHugo Herbelin
2019-05-31Remove Show Script (deprecated in 8.10)Gaëtan Gilbert
2019-05-28Fix [Drop. #use "include";;] for indirect_accessorGaëtan Gilbert
2019-05-27Overlay for mind_kelim change (#10133)Gaëtan Gilbert
2019-05-24Merge PR #10233: Fixing typos - Part 3Théo Zimmermann
Reviewed-by: Zimmi48
2019-05-24Update coqdev-setup-proofgeneral for duneGaëtan Gilbert
2019-05-24Adding overlays.Pierre-Marie Pédrot
2019-05-23Fixing typos - Part 3JPR
2019-05-23Merge PR #9895: [loadpath] Make loadpath handling self-contained and move to ↵Maxime Dénès
vernac Reviewed-by: maximedenes
2019-05-23Merge PR #10221: Fixing typos - Part 2 (reopening of #10218)Théo Zimmermann
2019-05-23Merge PR #10214: Better dune ocamldebug integrationEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-05-23Merge PR #10185: Remove undocumented Instance : ! syntaxVincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: vbgl
2019-05-23Fixing typos - Part 2JPR
2019-05-22Better dune ocamldebug integrationGaëtan Gilbert
- use coqc instead of coqtop (since -compile doesn't work anymore this is better) - pass through extra arguments to dune-dbg - auto detect the need to pass -emacs to ocamldebug - instructions for emacs users The dune-dbg dependencies are still broken ;_;
2019-05-22Merge PR #10177: Fix #10176: shadowing vs automatic class based ↵Hugo Herbelin
generalization + cleanups Reviewed-by: herbelin
2019-05-22Update build-system.txtFourchaux
2019-05-21Fixing typos - Part 1JPR
2019-05-21[loadpath] Further cleanup after merge with MlTop.Emilio Jesus Gallego Arias
We cleanup a bit the implementation of LoadPath which is not possible as now all the loadpath logic is in the same place. In particular, we remove exceptions in favor a `locate_result` monad. More cleanup should still be possible, in particular `locate_absolute_library` and `locate_qualified_library` should be merged.
2019-05-21Overlay for definition-not-visible overhaulGaëtan Gilbert
2019-05-21Overlay for removing Instance: !type syntaxGaëtan Gilbert
2019-05-17Overlay for removing Generalized 1st argGaëtan Gilbert
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: gares Ack-by: herbelin Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-05-14Merge PR #10164: Add aucontext debug printerPierre-Marie Pédrot
Reviewed-by: ppedrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
Ack-by: ejgallego Ack-by: maximedenes Reviewed-by: ppedrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Merge PR #10085: Do not include unreleased changelog in released versions.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: jfehrle Reviewed-by: vbgl
2019-05-13Merge PR #10076: [Canonical structures] Annotation to field declarations to ↵Enrico Tassi
prevent them from being “canonical” Ack-by: SkySkimmer Ack-by: Zimmi48 Reviewed-by: gares Ack-by: maximedenes Ack-by: robbertkrebbers Ack-by: vbgl
2019-05-13Merge PR #9887: [api] Remove 8.10 deprecations.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-05-13Add overlay for UnicoqMaxime Dénès
2019-05-13Make detyping robust w.r.t. indexed anonymous variablesMaxime Dénès
I don't think there's a reason to treat such variables more severely than unbound variables. This anomaly is often raised by debug printers (e.g. when studying complex scenarios using `Set Unification Debug`), and so makes debugging less convenient. Fixes #3754, fixes #10026.
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-14 22:36:13 +0000