| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
The old algorithm was relying on list membership, which is O(n). This was
nefarious for terms with many binders. We use instead sets in O(log n).
|
| |/
|
|
|
|
|
| |
Augment the "Illegal tactic application" error message with the number
of extra arguments passed.
Fixes BZ#5753.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.
We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.
Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).
We also fix a regression in the test-suite:
Mixing laziness and effects is a well-known hell. Here, an exception
that was raised for mere control purpose was delayed and raised at a
later time as an anomaly. We make the offending function eager.
|
| |\ |
|
| | | |
|
| | |
| |
| |
| | |
(from module List).
|
| |/ |
|
| |
|
|
| |
This fixes bug 5650: evar (x : Prop) should not be slow.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.
We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.
|
| | |/
|/| |
|
| |/
|
|
|
|
|
|
|
| |
Also taking into account a name in the return clause and in the
indices.
Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Reminder of (some of) the reasons for removal:
- Despite the claim in sigma.mli, it does *not* prevent evar
leaks, something like:
fun env evd ->
let (evd',ev) = new_evar env evd in
(evd,ev)
will typecheck even with Sigma-like type annotations (with a proof of
reflexivity)
- The API stayed embryonic. Even typing functions were not ported to
Sigma.
- Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly
less unsafe ones (e.g. s_enter), but those ones were not marked unsafe
at all (despite still being so).
- There was no good story for higher order functions manipulating evar
maps. Without higher order, one can most of the time get away with
reusing the same name for the updated evar map.
- Most of the code doing complex things with evar maps was using unsafe
casts to sigma. This code should be fixed, but this is an orthogonal
issue.
Of course, this was showing a nice and elegant use of GADTs, but the
cost/benefit ratio in practice did not seem good.
|
| |\
| |
| |
| | |
ssreflect and coq code
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
a flag suspectingly renamed in a clearer way
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As per https://github.com/coq/coq/pull/716#issuecomment-305140839
Partially using
```bash
git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i
```
and
```bash
git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i
```
The rest were manually edited by looking at the results of
```bash
git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less
```
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The new function is interp_glob_closure which is basically a renaming
and generalization of interp_uconstr.
Note a change of semantics that I could however not observe in
practice.
Formerly, interp_uconstr discarded ltac variables bound to names for
interning, but interp_constr did not. Now, both discard them.
We also export the new interp_glob_closure.
|
| | | |/
| | |
| | |
| | |
| | |
| | |
| | | |
This simplifies the API as before, inference of instances of type
classes was iff a type constraint was given.
We then export these both versions of interp_open_constr.
|
| | |/
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
evars.
This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.
Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
|
| |/
|
|
| |
a goal with unresolved evars.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
|
| | | |/
| |/|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes an inconsistency introduced in 554a6c806 (svn r12603) where
both interp_constr_with_bindings and interp_open_constr_with_bindings
were going through interp_open_constr (no type classes so as to not to
commit too early on irreversible choices, accepting unresolved holes).
We fix this by having interp_constr_with_bindings going to
interp_constr (using type classes and failing on unresolved evars).
The external impact is that any TACTIC EXTEND which refers to
constr_with_binding has now to decide whether it intends it to use
what the name suggest (using type classes and to fail if evars remain
unresolved), thus keeping constr_with_binding, or the actual behavior
which requires to use open_constr_with_bindings for strict
compatibility.
|
| | | | |
|
| | |/ |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.
This provides significantly clearer code for the AST, and is robust
wrt attributes.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | |
| |
| |
| | |
Now it is a private field, locations are optional.
|
| | |
| |
| |
| | |
One case missing due the TACTIC EXTEND macro.
|
| | | |
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
This is the second patch, which is a bit more invasive. We reasoning
is similar to the previous patch.
Code is not as clean as it could as we would need to convert
`glob_constr` to located too, then a few parts could just map the
location.
|
| |\ |
|
| | | |
|
Maxime Dénès
Pierre-Marie Pédrot
Tej Chajed
Hugo Herbelin
Emilio Jesus Gallego Arias
Matej Košík
Jason Gross
Gaetan Gilbert