aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-06-08Merge PR #10318: Test goal range in "only" selectorsPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2019-06-08Merge PR #10263: [proofs] Remove unused API [detected by coverage]Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2019-06-08Fix #10339: Anomaly in Ltac2.Pierre-Marie Pédrot
We use a user-facing wrapper instead of a low-level function raising internal exceptions.
2019-06-08[Test-suite] Add non-regression test case for #8725Vincent Laporte
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-08Adding a new kind of assumption to track assumption coming from "Context".Hugo Herbelin
This is to avoid depending on the combination "Discharge" + no opened section to trigger an automatic declaration of instance.
2019-06-08Test goal range in "only" selectorsGaëtan Gilbert
I don't know what goal_selector.v was supposed to test but CI says nobody relied on it.
2019-06-08Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ↵Pierre-Marie Pédrot
interpretation scopes Reviewed-by: Zimmi48 Reviewed-by: ppedrot Ack-by: vbgl
2019-06-08Updated changelog.Hugo Herbelin
2019-06-08Mini fix documentation coqtop in passing.Hugo Herbelin
2019-06-08Documenting new options -require-import, -require-export, etc.Hugo Herbelin
Slight improving of style in passing.
2019-06-08Command line: adding variants for Require, aligning on the vernac syntax.Hugo Herbelin
We deprecate -require (= Require Import) to avoid the confusion with Require. We propose a regular equivalent to all vernac variants in expanded and short version: -require-import, -require-export -require-import-from, -require-export-from -ri, -re -rifrom, -refrom We also add -rfrom, but wait for the end of deprecation of -require to replace -load-vernac-object by -require and to introduce a shorthand -r for the new -require.
2019-06-07Merge PR #10236: Update coqdev-setup-proofgeneral for duneEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Ack-by: ejgallego
2019-06-07Merge PR #10330: Dune: run coqc with -w +defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-07Merge PR #10335: simple IO CI branch is now `master`Emilio Jesus Gallego Arias
2019-06-07Merge PR #10311: Ltac2 codeowner / changelogMaxime Dénès
Reviewed-by: maximedenes
2019-06-07simple IO CI branch is now `master`Gaëtan Gilbert
2019-06-07Merge PR #10308: Merge the two sources of monomorphic constraints for ↵Gaëtan Gilbert
side-effects Reviewed-by: SkySkimmer
2019-06-07test suite: don't try to coqchk failed testsGaëtan Gilbert
2019-06-07Update changelog for 103032 and 10305Enrico Tassi
2019-06-07Dune: run coqc with -w +defaultGaëtan Gilbert
This matches the makefile build with -warn-error.
2019-06-07Merge PR #10205: Make discriminate tactic compatible with HoTTPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: mattam82 Reviewed-by: ppedrot
2019-06-07Fix bug #5710Claude Stolze
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
2019-06-06Make discriminate tactic compatible with HoTTAndreas Lynge
2019-06-06Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and ↵Pierre-Marie Pédrot
explain more Ack-by: SkySkimmer Reviewed-by: gares Reviewed-by: ppedrot Ack-by: tlringer
2019-06-06Merge PR #10278: vernac_load doesn't get a ?proof argumentEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: gares
2019-06-06Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.Vincent Laporte
Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: vbgl
2019-06-06Doc for per commit compile lintGaëtan Gilbert
2019-06-06CI: Test ml compilation of each commit in a PR in lint jobGaëtan Gilbert
2019-06-06Merge PR #10323: Remove old overlaysEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-06-06Merge the two sources of monomorphic constraints for side-effects.Pierre-Marie Pédrot
Instead of having the monormorphic universes from the immediate data separated from the ones from the body, we only rely on the former. There is no reason to delay given that the body is always force upfront.
2019-06-06Merge PR #10299: Lazy substitution of section contexts in opaque proofsMaxime Dénès
Reviewed-by: gares Ack-by: maximedenes Ack-by: ppedrot
2019-06-06Fix panel behavior as requested by #10292Claude Stolze
2019-06-06Remove old overlaysGaëtan Gilbert
I updated the readme example using the most recent overlay with only 1 touched development.
2019-06-06Update changes.rst as a follow-up to #9743Kazuhiko Sakaguchi
2019-06-06Update doc/changelog/03-notations/10180-deprecate-notations.rstMaxime Dénès
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
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-06Clean, document, and expand plugin tutorials 0 and 1Talia Ringer
2019-06-06[Ltac2] Interpretation scopes in “constr” arguments of tactic notationsVincent Laporte
2019-06-06Merge PR #10305: Fix SSR (un)fold of polymorphic terms - issue 9336Enrico Tassi
Reviewed-by: gares
2019-06-06Merge PR #10302: Fix SSR 'case B:b' with universe polymorphic equalityEnrico Tassi
Ack-by: andreaslyn Reviewed-by: gares
2019-06-06`deprecated` attribute support for notations and syntactic definitionsMaxime Dénès
We also slightly change the semantics of the `compat` syntax modifier to re-express it in terms of the `deprecated` attribute, and we deprecate it in favor of the latter.
2019-06-05Add Andreas Lynge to CREDITSAndreas Lynge
2019-06-05Remove redundancies in the INSTALL doc.Théo Zimmermann
2019-06-05Changelog entry for Ltac2 (missing from #10002).Théo Zimmermann
2019-06-05Add codeowner for Ltac2. Forgotten in #10002.Théo Zimmermann
Who should be secondary owner?
2019-06-05Fix #10283: clearer dependency documentation for building CoqIDE.Théo Zimmermann
2019-06-05vernac_load doesn't get a ?proof argumentGaëtan Gilbert
AFAICT the stm never gives Load a non-None ?proof.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 02:42:15 +0000