aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2019-07-08Merge PR #10246: Investigations in the initialization of coq binaries and ↵Emilio Jesus Gallego Arias
command line (part 1) Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin
2019-07-08Usage: bypassing a useless detour via a reference.Hugo Herbelin
2019-07-08An even more uniform treatment of the -help option across executables.Hugo Herbelin
Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s.
2019-07-08Removing -filterops "hack" from coqtop.Hugo Herbelin
This is now the "coqidetop" binary which specifically know how to collect extra arguments.
2019-07-08Some common points between coqc and other coq binaries.Hugo Herbelin
- Binding coqc execution to the generic support for Coq binaries (i.e. to start_coq). - Moving init_toploop to the init part of coq executables so that coqc can avoid to call it. By the way, it is unclear what workerloop should do with it. Also, it is unclear how much the -l option should be considered an coqidetop or coq*worker option. In any case, it should be disallowed in coqc, I guess? - Moving the custom init part at the end of the initialization phase. Seems ok, despites the few involved side effects.
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
We lose track of it at some time in "known_state" and assume that the reference cur_opt has not been modified in between the time it was set (in "new_doc") and "known_state".
2019-07-08Layout/documentation updates.Hugo Herbelin
2019-07-08An attempt to reorganize further coqtop initialization into semantic units.Hugo Herbelin
Incidentally moving parsing of "-batch" to the coqtop binary.
2019-07-08Adding methods help and parse_extra to custom toplevels data.Hugo Herbelin
In particular, method init does not do parsing any more. This allows for instance to let coqidetop treats itself the "-filteropts" option.
2019-07-08Function print_memory_stat: getting rid of a mutable.Hugo Herbelin
2019-07-08A classification of command line options.Hugo Herbelin
A few semantic changes: - several queries (-where, -config, ...) are accepted - queries are exclusive of other arguments - option -filterops is exclusive of other arguments if it contains another query (this allows to get rid of the "exitcode" hack)
2019-07-08Toplevel: structuring init_toplevel.Hugo Herbelin
2019-07-08Toplevel: structuring source code.Hugo Herbelin
2019-07-06Merge PR #10490: Dockerfile: update menhir versionEmilio Jesus Gallego Arias
2019-07-06Merge PR #10482: Use Format.pp_print_list with conditional instead of fold ↵Emilio Jesus Gallego Arias
for list prints in gramlib Reviewed-by: ejgallego
2019-07-06[Dockerfile] update menhir versionGaëtan Gilbert
Compcert needs a new menhir.
2019-07-05Merge PR #10484: Correct doc about default value for Typeclasses Dependency ↵Théo Zimmermann
Order Reviewed-by: Zimmi48
2019-07-05Use Format.pp_print_list with conditional instead of fold for list prints in ↵Gaëtan Gilbert
gramlib This means we don't need to ignore the result of the fold. cf #10471 Using Format.pp_print_list instead of a custom iteri was suggested by Jean-Christophe Léchenet (eponier)
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:10:32 +0000