aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-23Bump version numbersEnrico Tassi
2020-11-23Merge PR #11841: Distinguishing entry "ident" from entry "name" in term ↵coqbot-app[bot]
notations. Reviewed-by: jfehrle Reviewed-by: gares Reviewed-by: Zimmi48 Reviewed-by: maximedenes
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-22Updating doc wrt addition of grammar subentry "name" and deprecation of "ident".Hugo Herbelin
For constr, this means clarifying that "ident" is deprecated and to be replaced by "name". Here, some cleaning shall have to be done at the end of deprecation phase, when "ident" will take its literal meaning. For custom notations, this is about documenting the effect of "ident" and "global" which was yet undocumented. Note that we anticipate an example in constr working with the literal meaning of "ident" (temporarily silencing the warning). Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-22Adapting standard library, doc and test suite to ident->name renaming.Hugo Herbelin
2020-11-22Uniformizing indentation in ppvernac.ml.Hugo Herbelin
2020-11-22Renaming "ident" into "name" in grammar entries, to prevent confusions.Hugo Herbelin
We use a deprecation phase where: - "ident" means "name" (as it used to mean), except in custom coercion entries where it already meant "ident". - "ident" will be made again available (outside situation of coercions) to mean "ident" at the end of deprecation phase. Also renaming "as ident" into "as name". Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 19:03:00 +0000