aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-03-19[obligations] Step towards more structured handling of remaining obligations.Emilio Jesus Gallego Arias
There is a lot of check overhead in the code, we will try to provide a more convenient API for manipulation of remaining obligations.
2020-03-19[obligations] Refactor some common code on save pathEmilio Jesus Gallego Arias
Both the interactive and non-interactive save path share some internal table update code.
2020-03-19[obligations] More progress towards unification of the save pathEmilio Jesus Gallego Arias
We make internal types `private` as an step towards the unification of the save path with the rest of the system. In particular, this is allow us to guarantee invariants w.r.t. external users as the large majority of fields are always constant. This will also enable at some point a common creation of proof entry with the rest of the system.
2020-03-19[comFixpoint] Cleanup on opens prior to fix unificationEmilio Jesus Gallego Arias
2020-03-19[proof] Remove duplicated poly field in Proof_global.tEmilio Jesus Gallego Arias
2020-03-19[pfedit] Labelize sign parameterEmilio Jesus Gallego Arias
2020-03-19[declare] Remaining bits on the consistency of UState.t namingEmilio Jesus Gallego Arias
2020-03-19[vernac] Make local exception localEmilio Jesus Gallego Arias
2020-03-19[comFixpoing] Refactor hybrid interactive command modalityEmilio Jesus Gallego Arias
2020-03-19[lemmas] Fix comment on public APIEmilio Jesus Gallego Arias
After we moved `start_lemma_com` to `vernacentries` the comment on `start_lemma_with_initialization` needs update.
2020-03-19[lemma] Remove double normalization of typesEmilio Jesus Gallego Arias
It should be safe now after previous refactoring in lemmas.
2020-03-19[declare/lemmas] Make inference hook exception-freeEmilio Jesus Gallego Arias
This is a step towards cleanup of the `start` lemma path.
2020-03-19[ci] Overlays for declare interface refactoring.Emilio Jesus Gallego Arias
2020-03-19[declare] Remove one use of inline_private_constantsEmilio Jesus Gallego Arias
We instead favor the `build_by_tactic` function which should at some point better integrated in the declare core.
2020-03-19[declare] More uniformity in arguments labels / namesEmilio Jesus Gallego Arias
In anticipation for more consolidation of duplicated functionality.
2020-03-19[declare] Bring more consistency to parameters using labelsEmilio Jesus Gallego Arias
Most of the parameters were named, we fix the remaining cases.
2020-03-19Merge PR #11862: Fix deprecation warning in sphinx and remove workaround for ↵Théo Zimmermann
fixed bug Reviewed-by: Zimmi48
2020-03-19Merge PR #11745: Remove invisible U+FE00 variation selector from CoqIDE bindingsPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-19[refman] Stop using the deprecated math_block node (fixed GH-11856)Clément Pit-Claudel
2020-03-19[refman] Remove workaround for sphinx-doc/sphinx#4983Clément Pit-Claudel
2020-03-19Merge PR #11760: firstorder: default tactic is “auto with core”Théo Zimmermann
Reviewed-by: JasonGross Reviewed-by: Zimmi48
2020-03-19Merge PR #11860: [ci] [docker] Update to 4.09.1Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
Ack-by: herbelin
2020-03-19Merge PR #11822: Grants #11692: clear dependent knows about let-inPierre-Marie Pédrot
Reviewed-by: JasonGross Reviewed-by: ppedrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-19[stdlib] Remove a few `auto with *`Vincent Laporte
2020-03-18[ci] [docker] Update to 4.09.1Emilio Jesus Gallego Arias
That release includes non trivial changes related C compilers, in particular due to `-fno-common` support.
2020-03-18Merge PR #11607: Hide binder type in Ltac2Jason Gross
Reviewed-by: JasonGross Ack-by: SkySkimmer
2020-03-18Adding a round-trip test for binders.Pierre-Marie Pédrot
2020-03-18Actually use the binder type for Ltac2 that should be used in the kernel.Pierre-Marie Pédrot
That is, it contains the type of the binder so as not to rely on the relevance explicitly.
2020-03-18Hide the Ltac2 binder type.Pierre-Marie Pédrot
For robustness and it is better to leave it opaque. Users are not supposed to fiddle with it.
2020-03-18Merge PR #11559: Remove year in headers.Hugo Herbelin
Reviewed-by: jfehrle
2020-03-18Merge PR #11812: Add an Export locality to hintsThéo Zimmermann
Reviewed-by: Zimmi48 Ack-by: gares Ack-by: maximedenes
2020-03-18Merge PR #11839: Dead code in g_prim.mlgPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
Add headers to a few files which were missing them.
2020-03-18Adding overlays.Pierre-Marie Pédrot
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-18Export the user-facing attribute for hint locality.Pierre-Marie Pédrot
2020-03-18Also show unchanged headers.Théo Zimmermann
2020-03-18Remove dates in headers.Théo Zimmermann
Cf. discussion at #11559 and decision of Coq Call 2020-02-26.
2020-03-18Use a 3-valued flag for hint locality.Pierre-Marie Pédrot
We reuse the same type as for options, even though it is a bit ill-named. At least it allows to share code with it.
2020-03-18Hack a non-superglobal mode for hints.Pierre-Marie Pédrot
The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind.
2020-03-18Change some ouput tests due to the printing of implicitsSimonBoulier
2020-03-18Merge PR #11746: Register commonly used names from the Reals library for ↵Théo Zimmermann
plugins (e.g. gappa) Reviewed-by: Zimmi48
2020-03-17Merge PR #11699: Comment difference between the 2 hashes on constrPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-03-17Merge PR #11825: [ci] [docker] Update components in Docker imageGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Merge PR #11811: Remove a positivity check when Positivity Checking is offGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-03-17Add test for PR11811 (disable a positivity check)SimonBoulier
2020-03-17Dead code in g_prim.mlgHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:41:41 +0000