aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-18[api] Qualify access to `Nametab`Emilio Jesus Gallego Arias
In general, `Nametab` is not a module you want to open globally as it exposes very generic identifiers such as `push` or `global`. Thus, we remove all global opens and qualify `Nametab` access. The patch is small and confirms the hypothesis that `Nametab` access happens in few places thus it doesn't need a global open. It is also very convenient to be able to use `grep` to see accesses to the namespace table.
2018-10-18Merge PR #8761: [ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.Emilio Jesus Gallego Arias
2018-10-18[ci] Pin CI_REF to plugin_tutorial to use not yet merged commit.Théo Zimmermann
This fixes the CI until this commit is merged into master.
2018-10-18Merge PR #8756: [micromega] Build csdpcertVincent Laporte
2018-10-18Merge PR #8754: [doc] [build] Remove ocamlbuild leftovers.Théo Zimmermann
2018-10-17doc: mention ByteVectorYishuai Li
2018-10-17Strings: add ByteVectorYishuai Li
2018-10-17[micromega] Build csdpcertEmilio Jesus Gallego Arias
2018-10-17[doc] [build] Remove ocamlbuild leftovers.Emilio Jesus Gallego Arias
We had a brief leftovers of the ocamlbuild experiment that are not relevant anymore as it was removed from the tree a few years ago. p.s: The amount of cruft we have in the `dev/build/windows` folder is staggering, see for example what `git grep ocamlbuild` returns.
2018-10-17Enable fragile pattern warning in cclosureGaëtan Gilbert
This file is already mostly in the required style so I wanted to see what it looks like. For a couple matches I locally disabled the warning as it was too annoying otherwise (`when` clauses are especially annoying). There are a couple places where I think it clearly looks better (eg assoc_defined at the beginning of the file) but overall I'm not all that convinced. What do other people think?
2018-10-17Merge PR #8694: Various cleanups of universe apisPierre-Marie Pédrot
2018-10-17Merge PR #8710: [omega, btauto] Remove some dead codePierre-Marie Pédrot
2018-10-17[ci] [doc] Notes about branch names.Emilio Jesus Gallego Arias
I'd like to add this convention as it is very convenient for the development of dev tools. Example, I can do `setup-coq-devs ltac equations` and then get a fully composed tree. Similarly for preparing overlays.
2018-10-17Merge PR #8748: [dune] [plugins] Fix plugin name ground -> firstorderThéo Zimmermann
2018-10-17[build] Add dune file + fix warnings.Emilio Jesus Gallego Arias
This allows to drop the ltac2 folder inside the Coq dir and have it compose with the Coq build. I've fixed build warnings by the way.
2018-10-17[dune] [plugins] Fix plugin name ground -> firstorderEmilio Jesus Gallego Arias
This is needed for compatibility with directory-listing infrastructure.
2018-10-16Merge PR #8738: [clib] Deprecate string functions available in OCaml 4.05Pierre-Marie Pédrot
2018-10-16Merge PR #8742: [clib] Remove Array functions available in OCaml 4.05.0Pierre-Marie Pédrot
2018-10-16Merge PR #8059: Simplify code for [Definition := Eval ...]Matthieu Sozeau
2018-10-16{Univops->UState}.restrict_universe_contextGaëtan Gilbert
Thus the adhoc univops can be removed at the end of the deprecation period. Should we keep exposing restrict_universe_context or make people go through restrict? restrict_universe_context is used directly only by newring, where it's a choice between let univs = UState.restrict_universe_context univs vars in and let univs = UState.(context_set (restrict (of_context_set univs) vars)) in
2018-10-16{Univops -> Vars}.universes_of_constrGaëtan Gilbert
It's basically an occur check so it makes sense to put it in vars
2018-10-16UnivGen.extend_context -> Univ.extend_in_context_setGaëtan Gilbert
Such a basic function can live in Univ rather than the higher level UnivGen.
2018-10-16Deprecate UnivGen.new_{univ,Type,Type_sort}Gaëtan Gilbert
They are impractical since we need to get the level out to register it afterwards.
2018-10-16Clean UnivGen.fresh_instance APIGaëtan Gilbert
2018-10-16Deprecate univ-dropping UnivGen.new_sort_in_familyGaëtan Gilbert
2018-10-16Simplify UnivGen.type_of_referenceGaëtan Gilbert
2018-10-16UnivGen.constr_of_glob_univ -> Constr.mkRefGaëtan Gilbert
2018-10-16Remove [constr_of_global_in_context] in funindGaëtan Gilbert
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-16Simplify fresh_foo_instance functions and pretyping of univ instanceGaëtan Gilbert
2018-10-16Deprecate Global.universes_of_global (replaced by environ version)Gaëtan Gilbert
2018-10-16[Omega] Remove dead codeVincent Laporte
2018-10-16[btauto] Remove dead codeVincent Laporte
2018-10-16[omega] Remove dead codeVincent Laporte
2018-10-16Merge PR #8691: Remove some dead code in nsatz and micromega pluginsthery
2018-10-16[clib] Remove Array functions available in OCaml 4.05.0Emilio Jesus Gallego Arias
2018-10-16[clib] Deprecate string functions available in OCaml 4.05Emilio Jesus Gallego Arias
- `CString.strip -> String.trim` - `CString.split -> String.split_on_char` As noted by @ppedrot there are some small differences on semantics: > OCaml's `trim` also takes line feeds (LF) into account. Similarly, > OCaml's `split` never returns an empty list whereas Coq's `split` > does on the empty string.
2018-10-16[test-suite] Update csdp cacheVincent Laporte
2018-10-16[micromega] remove dead codeVincent Laporte
2018-10-16[nsatz] remove dead codeVincent Laporte
2018-10-16Document the issue with positive coinductive types.Pierre-Marie Pédrot
2018-10-16Merge PR #8695: Adding a functional version of constant- and ↵Pierre-Marie Pédrot
mind_of_delta_kn + functional version of is_polymorphic
2018-10-16Merge PR #8733: Implement ARGUMENT EXTEND in coqppEmilio Jesus Gallego Arias
2018-10-15Documenting the transition from camlp5 to coqpp for ARGUMENT EXTEND.Pierre-Marie Pédrot
2018-10-15Port remaining EXTEND ml4 files to coqpp.Pierre-Marie Pédrot
Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code.
2018-10-15Implement ARGUMENT EXTEND in coqpp.Pierre-Marie Pédrot
2018-10-15Plug ARGUMENT EXTEND into the argument extension API.Pierre-Marie Pédrot
2018-10-15Providing a centralized API for ARGUMENT EXTEND.Pierre-Marie Pédrot
We chose to stick to the most general possible API, even though the macro will not make full use of the possibilities. It makes explicit the various data expected to be provided in an orthogonal way.
2018-10-15Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT EXTEND macro.Pierre-Marie Pédrot
Those optional arguments did not really make sense. It was pretty clear from our code base, as all instances where triplicating the same type for TYPED, RAW_TYPED and GLOB_TYPED.
2018-10-15Merge PR #8689: A few useless accesses to the global environment in ↵Pierre-Marie Pédrot
pretyping and engine
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 02:37:32 +0000