aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-21Adding a regression test for bug #8785 (missing univ constraints registration).Hugo Herbelin
2018-10-20Merge PR #8769: [library] Remove redundant re-addition of universe constraints.Gaëtan Gilbert
2018-10-20Merge PR #8782: gitignore test-suite/.nia.cacheThéo Zimmermann
2018-10-19Merge PR #8758: [api] Qualify access to `Nametab`Hugo Herbelin
2018-10-19gitignore test-suite/.nia.cacheGaëtan Gilbert
This gets generated since 7f445d1027cbcedf91f446bc86afea36840728ba
2018-10-19Merge PR #8724: [universes] deprecate constr_of_globalPierre-Marie Pédrot
2018-10-19Merge PR #8740: Removing the Camlp5 macros from CLexer.Emilio Jesus Gallego Arias
2018-10-18[library] Remove redundant re-addition of universe constraints.Emilio Jesus Gallego Arias
After some analysis this should be taken care of by `Safe_typing.add_constant` It was added in https://github.com/coq/coq/commit/f7338257584ba69e7e815c7ef9ac0d24f0dec36c , so maybe @gares can provide more context as to how is this stuff supposed to work.
2018-10-18Merge PR #8719: [ci] [appveyor] Disable validate target.Maxime Dénès
2018-10-18Merge PR #8670: Document the issue with positive coinductive types.Théo Zimmermann
2018-10-18Adding a rule to generate grammar.cma.Pierre-Marie Pédrot
Since the removal of the dependency in camlp5 for CLexer, it looks like this file was never generated, leading to installation failure. We add it as a dependency of the install step.
2018-10-18Removing the Camlp5 macros from CLexer.Pierre-Marie Pédrot
We partially hand-translated so as to result in the minimal diff possible.
2018-10-18[universes] deprecate constr_of_globalMatthieu Sozeau
In favor of a constr_of_monomorphic_global function. When people move to the new Coqlib interface they will also see this deprecation message encouraging them to think about the best move. This commit changes a few references to constr_of_global and replaces them with a constr_of_monomorphic_global which makes it apparent that this is not the function to call to globalize polymorphic references. The remaining parts using constr_of_monomorphic_global are easily identifiable using this: omega, btauto, ring, funind and auto_ind_decl mainly (this fixes firstorder). What this means is that the symbols registered for these tactics have to be monomorphic for now.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:16:24 +0000