aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-07-05Merge PR #10484: Correct doc about default value for Typeclasses Dependency ↵Théo Zimmermann
Order Reviewed-by: Zimmi48
2019-07-05Correct doc about default value for Typeclasses Dependency OrderGaëtan Gilbert
2019-07-04Merge PR #10479: Fix miscellaneous mistakes in unreleased changelog entries.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-07-04Fix miscellaneous mistakes in unreleased changelog entries.Théo Zimmermann
2019-07-04Merge PR #10461: Simplify Declare.declare_variableEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-07-04Merge PR #10359: Remove dependency of native_compile on global env for symbolsMaxime Dénès
Reviewed-by: maximedenes Reviewed-by: ppedrot
2019-07-03Move variable_secpath logic to dumpglob from constrinternGaëtan Gilbert
2019-07-03Remove unused variable_path (note secpath is still used)Gaëtan Gilbert
2019-07-03declare_variable: path is always Lib.cwd()Gaëtan Gilbert
2019-07-03Remove unused Decls.variable_{context,polymorphic}Gaëtan Gilbert
2019-07-03Declare section variables in direct style "without" an objectGaëtan Gilbert
The object was mostly for wrangling universes, but we already have the universe object for that. It's also used by some code which iterates over objects to find variables. Search used to do this but was changed in a previous commit. Prettyp.print_context and derivatives do this and I don't understand it enough to fix it, so I kept a dummy object around. It seems like a not very common used Print family (not documented AFAICT) so maybe we should remove it all instead.
2019-07-03Move declare_universe_context to top of DeclareGaëtan Gilbert
In preparation for the other declarations to use it.
2019-07-03Search: do not use libobject to find variablesGaëtan Gilbert
In preparation for removing the VARIABLE object. It seems this doesn't change the output tests.
2019-07-03Safe_typing.push_named_assum: don't take universesGaëtan Gilbert
The caller should push them first
2019-07-03Remove constrintern global_level dead codeGaëtan Gilbert
Not sure what this was for.
2019-07-03Simplify (restrict_path 0 sp) -> (make_path DirPath.empty id)Gaëtan Gilbert
This is the only use of restrict_path so we just remove it. The name collision between Libnames.make_path (takes a dirpath) and Lib.make_path (uses current module+section path) is a bit awkward...
2019-07-03Merge PR #10442: Reify libobject containersEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-07-03Merge PR #10472: [vernac] Fix bad merge which resulted in code using wrong ↵Gaëtan Gilbert
module name. Reviewed-by: SkySkimmer
2019-07-03[vernac] Fix bad merge which resulted in wrong module name.Emilio Jesus Gallego Arias
2019-07-03Merge PR #10338: Fix #9455: avoid update_global_env when unchanged ↵Emilio Jesus Gallego Arias
Global.universes() Ack-by: SkySkimmer Reviewed-by: ejgallego Ack-by: gares
2019-07-03Merge PR #10467: [nix] python2 -> python3Vincent Laporte
Reviewed-by: vbgl
2019-07-03Merge PR #10419: [api] Refactor most of `Decl_kinds`Gaëtan Gilbert
Reviewed-by: SkySkimmer Ack-by: herbelin
2019-07-02[nix] python2 -> python3Théo Zimmermann
We are not supposed to have any script depending specifically on python2.
2019-07-02[ci] Overlays for #10419Emilio Jesus Gallego Arias
2019-07-02[test-suite] Fix evil plugin after changes in declare API.Emilio Jesus Gallego Arias
We should have this in the check target, but meanwhile we have to do manual housekeeping here.
2019-07-02[declare] Cleanup on imports, move exception.Emilio Jesus Gallego Arias
We cleanup a few imports on Declare, and indeed we find a suspicious exception `AlreadyDeclared` present in `CErrors` where it should not be there. We move it to `Declare`, waiting for more investigation.
2019-07-02Merge PR #10336: Improve the ambiguous paths warning to indicate which path ↵Gaëtan Gilbert
is ambiguous with new one Reviewed-by: SkySkimmer
2019-07-02Merge PR #10340: [vernac] Remove special status of Load, turn it into VtNoProofGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-07-02Improve the ambiguous paths warning to indicate which path is ambiguous with ↵Kazuhiko Sakaguchi
new one
2019-07-01[declare] Remove superfluous APIEmilio Jesus Gallego Arias
`declare_definition` didn't improve a lot the declare path and was used only once on interesting code. Also, it had many optional parameters. The declare path is critical enough as to care about a tidy API.
2019-07-01[decls] Remove goal_object_kind type.Emilio Jesus Gallego Arias
We can use logical kind for the same purpose, which is mainly dumpglob, so `goal_object_kind` was never matched against, making this transformation safe.
2019-07-01[api] Reduce declare_kinds even more.Emilio Jesus Gallego Arias
We remove two flags that were seldom used in favor of named parameters.
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
They are clearly not at the same importance level, thus we use a named parameter and isolate the kinds as to allow further improvements and refactoring.
2019-07-01[dumpglob] Move dumpglob-specific data to dumpglob.Emilio Jesus Gallego Arias
The whole business of cst_kind is fishy tho, it seems to me that it should be removed from the libobject path.
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
We move the bulk of `Decl_kinds` to a better place [namely `interp/decls`] and refactor the use of this information quite a bit. The information seems to be used almost only for `Dumpglob`, so it certainly should end there to achieve a cleaner core. Note the previous commits, as well as the annotations regarding the dubious use of the "variable" data managed by the `Decls` file. IMO this needs more work, but this should be a good start.
2019-07-01[pretyping] Remove seemingly unless check about "variable" opacity.Emilio Jesus Gallego Arias
See discussion in #10417
2019-07-01Merge PR #10433: [vernac] Cleanup on interface of VernacentriesGaëtan Gilbert
Reviewed-by: SkySkimmer
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: gares Ack-by: herbelin Ack-by: jfehrle
2019-06-28Merge PR #10438: Kernel transparent definition entries have no body universes.Pierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot
2019-06-28Merge PR #10434: [declare] Fine tuning of Hook type.Pierre-Marie Pédrot
Ack-by: ejgallego Reviewed-by: ppedrot
2019-06-28Reify libobject containersMaxime Dénès
We make a few libobject constructions (Module, Module Type, Include,...) first-class and rephrase their handling in direct style (removing the inversion of control). This makes it easier to define iterators over objects without hacks like inspecting the tags of dynamic objects.
2019-06-27Merge PR #10443: Fix dev/doc/README.md by removing redundant, outdated info.Clément Pit-Claudel
Reviewed-by: cpitclaudel
2019-06-27Fix dev/doc/README.md by removing redundant, outdated info.Théo Zimmermann
And also clean INSTALL file of useless reminder of the procedure to install using a package manager.
2019-06-27[vernac] Cleanup on interface of VernacentriesEmilio Jesus Gallego Arias
2019-06-27[extraction] Remove not very useful call to dumpglob.Emilio Jesus Gallego Arias
The old code was conditionally dumping and catching `Not_found`, as noted by Gaëtan Gilbert on #10433: > we could just remove the dump, the sibling functions > (`full_extraction`, etc...) don't bother to dump for instance.
2019-06-27Kernel transparent definition entries have no body universes.Gaëtan Gilbert
2019-06-27Merge PR #10429: Perform the opaque section variable inference outside of ↵Gaëtan Gilbert
the kernel Reviewed-by: SkySkimmer Reviewed-by: gares
2019-06-27[vernac] Remove special status of Load, turn it into VtNoProofEmilio Jesus Gallego Arias
State is still token except for proofs [due to the compat layer, would be great if someone could port the STM], but this should be good for now.
2019-06-27Merge PR #10337: [stm] [vernac] Remove special ?proof parameter from vernac ↵Enrico Tassi
main path Ack-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares
2019-06-26[ci] Overlays for #10337Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 21:41:44 +0000