aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-10-17doc: mention ByteVectorYishuai Li
2018-10-17Strings: add ByteVectorYishuai Li
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
2018-10-15Correct some spelling errorsBenjamin Barenblat
Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
2018-10-15Merge PR #8704: [vernac] Remove unused abstraction from declaration_hook type.Hugo Herbelin
2018-10-15Merge PR #8732: [ci] [sf] Remove sed hacks from the SF build.Gaëtan Gilbert
2018-10-14[ci] [sf] Remove sed hacks from the SF build.Emilio Jesus Gallego Arias
Fixes #8337
2018-10-14A useless occurrence of Global.env.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:45:08 +0000