aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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-09Merge PR #10245: Command line: adding variants for Require, aligning on the ↵Emilio Jesus Gallego Arias
vernac syntax Reviewed-by: cpitclaudel Reviewed-by: ejgallego Ack-by: herbelin
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-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-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-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-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-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-05Add Andreas Lynge to CREDITSAndreas Lynge
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-05vernac_load doesn't get a ?proof argumentGaëtan Gilbert
AFAICT the stm never gives Load a non-None ?proof.
2019-06-05Merge PR #10215: Refine typing of vernacular commandsMaxime Dénès
Reviewed-by: SkySkimmer Ack-by: ejgallego Ack-by: gares
2019-06-05Merge PR #10307: allow empty tactic_rules in ARGUMENT EXTENDPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-06-05Merge PR #10296: Unused ssr ntsEnrico Tassi
Reviewed-by: gares
2019-06-05allow empty tactic_rules in ARGUMENT EXTENDDabrowski
2019-06-04[vernac] Interpret regular vernacs symbolicallyEmilio Jesus Gallego Arias
This provides uniformity to the inner loop and prepares the way to export a refined type for interpretation. The only non-uniformity remaining is the one due to the `?proof` parameter; it won't be easy to fix due to upper layers issues. Note that this step is not yet fully satisfying, as a true typed `vernac_expr` definition is still not possible because of syntactic non-uniformity, in particular all the surgery done for `CoFixpoint` and `Instance` should be eliminated in favor of more refined AST tags. An interesting TODO is to handle attributes symbolically too, as to remove boilerplate.
2019-06-04Fix SSR (un)fold of polymorphic terms - issue 9336Andreas Lynge
2019-06-04Merge PR #10265: Fix #10264: Singleton class field data is erroneous.Matthieu Sozeau
Reviewed-by: mattam82
2019-06-04Fix SSR 'case B:b' with universe polymorphic equalityAndreas Lynge
2019-06-04Fix typo in changelogEnrico Tassi
2019-06-04Simplify vernacentries calls to classes, remove unused args, reject ↵Gaëtan Gilbert
deprecated attribute This code was significantly more complex than necessary.
2019-06-04[rewrite] remove program_mode from attributes (unused)Enrico Tassi
2019-06-04remove leftover commentsEnrico Tassi
2019-06-04update overlaysEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 18:28:17 +0000