aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-22Adding debugging printer for stacks of EConstr.Hugo Herbelin
2020-11-21Merge PR #12246: Adding support for applying in several hypotheses at the ↵Pierre-Marie Pédrot
same time (granting #9816) Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-21Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly ↵coqbot-app[bot]
fix #11170). Reviewed-by: gares Reviewed-by: xavierleroy Ack-by: ppedrot
2020-11-21Remove dependency on BinNat.Guillaume Melquiond
2020-11-20Merge PR #13248: Build all_stdlib.v in test suite makefilecoqbot-app[bot]
Reviewed-by: ejgallego
2020-11-20Merge PR #13265: Add support for general non-necessarily-recursive binders ↵coqbot-app[bot]
in notations Reviewed-by: ejgallego Ack-by: Zimmi48 Ack-by: jfehrle
2020-11-20Merge PR #13352: Configure default value of -native-compilercoqbot-app[bot]
Reviewed-by: erikmd Reviewed-by: silene Ack-by: mattam82 Ack-by: Blaisorblade Ack-by: gares Ack-by: Zimmi48 Ack-by: SkySkimmer Ack-by: ejgallego
2020-11-20Add a testcase.Guillaume Melquiond
2020-11-20Add changelog for #13265.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Tests for notations with general single (non-recursive) binders.Hugo Herbelin
2020-11-20Documentation of the support for general single binders in notations.Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-11-20Merge PR #13233: add perennial to benchmark suitePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-20Enforcing when a binding variable has no explicit type in constr_notation.Hugo Herbelin
This avoids relying on fragile invariants.
2020-11-20A step towards supporting pattern cast deeplier.Hugo Herbelin
We at least support a cast at the top of patterns in notations.
2020-11-20Add preliminary support for notations with large class (non-recursive) binders.Hugo Herbelin
We introduce a class of open binders which includes "x", "x:t", "'pat" and a class of closed binders which includes "x", "(x:t)", "'pat".
2020-11-20Rewriting convoluted code of set_var_scope in constrintern.ml.Hugo Herbelin
2020-11-20Add changelogPierre Roux
2020-11-20[CI] Deactivate native-compiler in some jobsPierre Roux
A few libraries in the CI don't compile with it (out of memory).
2020-11-20[CI] Deactivate native-compiler for a few tests that fail with itPierre Roux
2020-11-20[CI] Update coq_makefilePierre Roux
2020-11-20Add default value of -native-compiler to `coqc -config`Pierre Roux
2020-11-20Configure default value of -native-compilerPierre Roux
This an implementation of point 2 of CEP coq/ceps#48 https://github.com/coq/ceps/pull/48 Option -native-compiler of the configure script now impacts the default value of the option -native-compiler of coqc. The -native-compiler option of the configure script is added an ondemand value, which becomes the default, thus preserving the previous default behavior. The stdlib is still precompiled when configuring with -native-compiler yes. It is not precompiled otherwise.
2020-11-20Make sure accumulators do not exceed the minor heap (partly fix #11170).Guillaume Melquiond
Accumulators can grow arbitrarily large, even when well-typed. So, this commit makes sure they are allocated on the major heap when they are too large. If so, fields need to be filled with caml_initialize, in case they point to the minor heap.
2020-11-20Merge PR #12965: Fixes #9569: in notations with binders, prevent collisions ↵coqbot-app[bot]
between variable and non-qualified global references Reviewed-by: ejgallego Ack-by: maximedenes Ack-by: gares
2020-11-20Build all_stdlib.v in test suite makefileGaëtan Gilbert
instead of recursive make
2020-11-20Merge PR #13425: [stm] [declare] Try to propagate safe bits of proof informationcoqbot-app[bot]
Reviewed-by: gares
2020-11-20Merge PR #13426: [doc] [ssr] fix documentation of reflectcoqbot-app[bot]
Reviewed-by: CohenCyril
2020-11-20Merge PR #13399: Miscellaneous ring improvements in code + error messagesPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-20add perennial to benchmark suiteRalf Jung
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Merge PR #13305: Only lower inductives to Prop if the type is syntactically ↵Pierre-Marie Pédrot
an arity. Reviewed-by: ppedrot
2020-11-20Adding change log.Hugo Herbelin
2020-11-20Granting #9816: apply in takes several hypotheses.Hugo Herbelin
2020-11-20Merge PR #13360: Fix incorrect name refreshing when interning a generalized ↵coqbot-app[bot]
binder Reviewed-by: herbelin
2020-11-20Merge PR #13403: Use only nats for occs_nums rather than intscoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: herbelin
2020-11-20[doc] [ssr] fix documentation of reflectEnrico Tassi
2020-11-20Update ↵Hugo Herbelin
doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst Co-authored-by: Enrico Tassi <Enrico.Tassi@inria.fr>
2020-11-20Merge PR #13386: Fixes #9971: a useless situation where the type of a ↵coqbot-app[bot]
primitive projection was wrongly supposed to be already inferred Reviewed-by: gares
2020-11-20Merge PR #13371: Extend hack to use postponed constraints in retyping to ↵coqbot-app[bot]
template poly Reviewed-by: gares Reviewed-by: herbelin
2020-11-20[stm] [declare] Remove pinfo internals hack.Emilio Jesus Gallego Arias
After the previous commit, the stm should correctly pass proof information, thus we make `proof_object` carry it removing a bunch of internal code.
2020-11-20[stm] [declare] Try to propagate safe bits of proof informationEmilio Jesus Gallego Arias
Since 8.5, the STM could not delegate proof information it was contained inside a closure. This could potentially create some problems, as witnessed in #12586. Recent refactoring have reified however much of this state, so it seems a good idea to use bits of the state now, at the cost of introducing some safeguards in `declare.ml` w.r.t. `Ephemerons`.
2020-11-19Adding changelog for #13237.Hugo Herbelin
2020-11-19Merge PR #13423: [changelog] Indicate a replacement for deprecated syntax of ↵coqbot-app[bot]
debug / info_eauto. Reviewed-by: jfehrle
2020-11-19[changelog] Indicate a replacement for deprecated syntax of debug / info_eauto.Théo Zimmermann
2020-11-19Add overlays for elpi and unicoq.Hugo Herbelin
2020-11-19Add changelog for #13386.Hugo Herbelin
2020-11-19Use a proper canonical structure entry for projections.Hugo Herbelin
This is to make more explicit that arguments of the projection are not kept. We seize this opportunity to use QGlobRef equality on GlobRef.
2020-11-19Fixes #9971: expand_projections failing on primitive projections of unknown ↵Hugo Herbelin
type. This was a case where expand_projections was calling find_mrectype which was expecting the argument of the projection to be an inductive. We could have ensured that this type is at least the appropriate inductive applied to fresh evars, but this expand_projections was in practice used for checking the applicability of canonical structures and the unifiability of the parameters of the projections is anyway a consequence of the unifiability of the principal argument of the projections. So, the latter is enough.
2020-11-19Merge PR #13421: Fix typo in rst link syntax.coqbot-app[bot]
Reviewed-by: jfehrle
2020-11-19Fix typo in rst link syntax.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 12:15:42 +0000