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-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-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-17Merge PR #8748: [dune] [plugins] Fix plugin name ground -> firstorderThéo Zimmermann
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-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
2018-10-15Merge PR #8589: Correct some spelling errors (continued)Emilio Jesus Gallego Arias
2018-10-15Merge PR #8717: Lemmas, DeclareDef: internal reorganization of code ↵Emilio Jesus Gallego Arias
highlighting what can be shared
2018-10-15Mini-factorization preparing unification.Hugo Herbelin
2018-10-15Make code of `Lemmas.save` closer to the one of `DeclareDef.declare_definition`.Hugo Herbelin
This is a theoretical change of semantics in the presence of commands generating a "hook", such as "Coercion c := ...", or "SubClass", or "Canonical Structure". However, none of these commands have a "Discharge" effect, so the case was not used.
2018-10-15DeclareDef: Reorganizing declaration of definitions in a more structured way.Hugo Herbelin
In particular, we highlight the similarities and differences between local and global definitions.
2018-10-15Merge PR #8716: Lemmas: Little simplification of artificially convoluted codeEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:38:22 +0000