| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #12785: Ltac2 Performance Overhead.
|
|
Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.
This should be 1:1 equivalent to the previous code, we are just moving code
around.
|
|
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: SkySkimmer
Ack-by: ppedrot
Ack-by: ejgallego
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: jfehrle
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
`coe_source` and `coe_target` fields of type `cl_typ` have been added to
`coe_info_typ` so that it allows querying the classes from a `GlobRef.t` of a
coercion. The `coercion` record has also been replaced with `coe_info_typ`.
|
|
The table of coercion classes `class_tab` is now indexed by `cl_typ` instead of
integers (`cl_index`). All the uses of `cl_index` and `Bijint` have been
replaced with `cl_typ` and `ClTypMap` respectively.
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
|
|
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: JasonGross
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: ppedrot
|
|
solve_constraints
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
To get the right version of git to use the list-contributors.sh script.
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: ppedrot
Reviewed-by: ejgallego
|
|
|
|
|
|
By separating the libobject for create db and other hints we can unify
handling of local/superglobal.
|
|
|
|
|
|
|
|
|
|
ssreflect asks setoid rewrite to rewrite in goal
"forall_special_name_ : T, _other_name_"
Since this is a non dependent product, setoid rewrite converts that to
"impl T _other_name_" and must be taught to restore the special name
when unfolding impl.
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: gares
Ack-by: LasseBlaauwbroek
Ack-by: silene
Ack-by: vbgl
|
|
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.
|
|
raised.
Reviewed-by: jfehrle
|
|
Reviewed-by: jfehrle
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Now that they are well described on the website.
|
