| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Fixes #13453 which was a loop in
~~~ocaml
let normalize a =
let o = optims () in
let rec norm a =
let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
if eq_ml_ast a a' then a else norm a'
in norm a
~~~
the `eq_ml_ast` was always returning `false`.
|
|
notations.
Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: ppedrot
|
|
erroneously caught
Reviewed-by: ppedrot
|
|
sense
Reviewed-by: Zimmi48
|
|
|
|
|
|
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>
|
|
|
|
|
|
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>
|
|
|
|
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.
|
|
same time (granting #9816)
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
fix #11170).
Reviewed-by: gares
Reviewed-by: xavierleroy
Ack-by: ppedrot
|
|
|
|
semantic.
|
|
|
|
|
|
Also includes minor layout or code changes.
|
|
We also align their type on (more) standard invariants.
|
|
|
|
In #11172, an "=" on the number of arguments of an applied coercion
had become a ">" on the number of arguments of the coercion. It should
have been a ">=". The rest of changes in constrextern.ml is "cosmetic".
Note that in #11172, in the case of a coercion to funclass, the
definition of number of arguments of an applied coercion had moved
from including the extra arguments of the coercion to funclass to
exactly the nomber of arguments of the coercion (excluding the extra
arguments). This was necessary to take into account that several
coercions can be nested, at least of those involving a coercion to
funclass.
Incidentally, we create a dedicated output file for notations and
coercions.
|
|
|
|
The Norm name was confusing enough to have introduced a few kernel
bugs, so it deserved to be changed as suggested in #13274.
Contrarily to what it seemingly meant, it was actually standing
for neutral terms rather than normal ones. I have kept the 4-letter
naming scheme for simplicity and renamed it into Ntrl.
|
|
Reviewed-by: ejgallego
|
|
in notations
Reviewed-by: ejgallego
Ack-by: Zimmi48
Ack-by: jfehrle
|
|
Reviewed-by: erikmd
Reviewed-by: silene
Ack-by: mattam82
Ack-by: Blaisorblade
Ack-by: gares
Ack-by: Zimmi48
Ack-by: SkySkimmer
Ack-by: ejgallego
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
Reviewed-by: ppedrot
|
|
This avoids relying on fragile invariants.
|
|
We at least support a cast at the top of patterns in notations.
|
|
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".
|
|
|
|
|
|
A few libraries in the CI don't compile with it
(out of memory).
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
between variable and non-qualified global references
Reviewed-by: ejgallego
Ack-by: maximedenes
Ack-by: gares
|
|
instead of recursive make
|
|
Reviewed-by: gares
|
|
Reviewed-by: CohenCyril
|
