aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-23Merge PR #13446: Adding debugging printer for stacks on EConstrPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-11-23Merge PR #13377: Fix timeout by ensuring signal exceptions are not ↵Pierre-Marie Pédrot
erroneously caught Reviewed-by: ppedrot
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-22Adding debugging printer for stacks of EConstr.Hugo Herbelin
2020-11-22Fix timeout by ensuring signal exceptions are not erroneously caughtLasse Blaauwbroek
Fixes #7430 and fixes #10968 This commit makes the following changes: - Add an exception `Signal` used to convert OCaml signals to exceptions. `Signal` is registered as critical in `CErrors` to avoid being caught in the wrong `with` clauses. - Make `Control.timeout` into a safer interface based on `option` instead of exceptions. - Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of `Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation. - Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.
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-20Use nat_or_var where negative values don't make senseJim Fehrle
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:44:11 +0000