| Age | Commit message (Collapse) | Author |
|---|
|
instead of catching `Not_found`
Reviewed-by: ppedrot
|
|
catching `Not_found`
`Global.lookup_constant` fails with an assertion instead of `Not_found`. Some
code relied upon `Not_found`.
|
|
registered
|
|
Reviewed-by: mattam82
|
|
The old code was generating different patterns, depending on whether
a projection with parameters was expanded or not. In the first case,
parameters were present, whereas in the latter they were not.
We fix this by adding dummy parameter arguments on sight.
Fixes #14009: TC search failure with primitive projections.
|
|
As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.
It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.
We thus remove all bitrotten dead code.
|
|
|
|
Reviewed-by: ppedrot
|
|
As a bonus ltac2 can produce bullet suggestions.
|
|
This is more consistent with other code.
|
|
Reviewed-by: SkySkimmer
|
|
We factorize the code for replace and subst, since it seems there is no
reason to keep them separate, not even performance. Some static invariants are
made explicit in the API.
|
|
Instead of recomputing the n-th lifts of terms for every subterm under a context,
we introduce a table storing the value of this lift across contexts. While not
the most efficient algorithmically, it is still much more efficient in practice and
does not exhibit the exponential behaviour of replacing under different subcontexts.
In an ideal world we would have an equality function on terms that allows to compute
equality up to lifts, which would prevent having to even compute the lift at all, but
the current fix has the advantage to be self-contained and not require dangerous
tweaking of an equality function which is already complex enough as it is.
Fixes #13896: cbn very slow.
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
They were unconditionally set to true, leading to a lot of dead branches.
|
|
By separating the libobject for create db and other hints we can unify
handling of local/superglobal.
|
|
We introduce a new package structure for Coq:
- `coq-core`: Coq's OCaml tools code and plugins
- `coq-stdlib`: Coq's stdlib [.vo files]
- `coq`: meta-package that pulls `coq-{core,stdlib}`
This has several advantages, in particular it allows to install Coq
without the stdlib which is useful in several scenarios, it also open
the door towards a versioning of the stdlib at the package level.
The main user-visible change is that Coq's ML development files now
live in `$lib/coq-core`, for compatibility in the regular build we
install a symlink and support both setups for a while.
Note that plugin developers and even `coq_makefile` should actually
rely on `ocamlfind` to locate Coq's OCaml libs as to be more robust.
There is a transient state where we actually look for both
`$coqlib/plugins` and `$coqlib/../coq-core/plugins` as to support
the non-ocamlfind plus custom variables.
This will be much improved once #13617 is merged (which requires this
PR first), then, we will introduce a `coq.boot` library so finally
`coqdep`, `coqchk`, etc... can share the same path setup code.
IMHO the plan should work fine.
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: mattam82
|
|
|
|
pattern
Reviewed-by: ppedrot
|
|
|
|
|
|
We compute earlier if "apply in" clears or not.
We inline prepare_naming into its only client prepare_intros_opt
(using the more general make_naming instead).
|
|
We build earlier the final expected name at the end of a sequence of
"%" introduction patterns.
|
|
|
|
This also allows to move the strong variant of cbn to the Cbn module.
|
|
We deprecate unspecified locality as was done for Hint.
Close #13724
|
|
|
|
|
|
We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
|
|
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
|
|
Reviewed-by: mattam82
Reviewed-by: gares
Ack-by: SkySkimmer
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
We move bind_red_expr_occurrences from Tactics to Redexpr, where it
semantically belongs. We also hide it and seal the corresponding evaluated
types.
|
|
This was a source of slowdown observed in bedrock2.
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: gares
|
|
|
|
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
|
