| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Instead of recomputing the evar name environment from scratch when it is
unchanged, we simply return the original one.
This should fix #4964 for good, although I still find the global evar naming
mechanism from Pretyping more than messy. Introducing the heuristic allowing
to capture variables from Ltac in constr binders is indeed the root of many
evils... That is far from being a zero-cost abstraction!
|
| | | |
|
| |/
|
|
|
|
|
|
|
| |
This is a followup to 91ee24b4a7843793a84950379277d92992ba1651 , where
we got a few cases wrong wrt to newline endings.
Thanks to @herbelin for pointing it out.
This doesn't yet fix https://coq.inria.fr/bugs/show_bug.cgi?id=4842
|
| |
|
|
|
|
|
|
| |
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
|
| |\
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We used to recompute all fresh named contexts for evars before this patch in
the push_rel_context_to_named_context function. This was incurring a linear
penalty and a memory explosion due to the reallocation of many arrays. Now, we
rather remember the context between evar creations by sharing it in the pretyping
environment.
This can be considered as a fix for bug #4964 even though we might do better.
|
| | | |
|
| | |
| |
| |
| | |
This saves a quadratic allocation by replacing arrays with maps.
|
| | |
| |
| |
| |
| | |
In addition to sharing, we also delay the computation of the environment in
a by-need fashion.
|
| |/ |
|
| |
|
|
|
|
|
| |
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.
Minor change of the API (adding one error case to recursion_scheme_error).
|
| |/ /
| |
| |
| | |
They were allowing algebraic universes to slip in terms.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Because refreshing Prop is not semantics-preserving,
the new universe is >= Set, so cannot be minimized to Prop
afterwards.
|
| | |/
| |
| |
| |
| |
| |
| | |
In congruence, refresh universes including the Set/Prop ones so that
congruence works with cumulativity, not restricting itself to the
inferred types of terms that are manipulated but allowing them to be
used at more general types. This fixes bug #4609.
|
| | |
| |
| |
| | |
For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
|
| | |
| |
| |
| |
| |
| | |
module)
For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
|
| | | |
|
| | |
| |
| |
| |
| | |
whd_zeta now takes an evar_map and looks in evar instances. This changes
the behavior of whd_zeta e.g. on let x := ?t in x
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a reimplementation of Hugo's PR#117.
We are trying to address the problem that the name of some reduction functions
was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in
reduction). Like PR#117, we are careful that no function changed semantics
without changing the names. Porting existing ML code should be a matter of
renamings a few function calls.
Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX
collectively denominated iota.
We renamed the following functions:
Closure.betadeltaiota -> Closure.all
Closure.betadeltaiotanolet -> Closure.allnolet
Reductionops.beta -> Closure.beta
Reductionops.zeta -> Closure.zeta
Reductionops.betaiota -> Closure.betaiota
Reductionops.betaiotazeta -> Closure.betaiotazeta
Reductionops.delta -> Closure.delta
Reductionops.betalet -> Closure.betazeta
Reductionops.betadelta -> Closure.betadeltazeta
Reductionops.betadeltaiota -> Closure.all
Reductionops.betadeltaiotanolet -> Closure.allnolet
Closure.no_red -> Closure.nored
Reductionops.nored -> Closure.nored
Reductionops.nf_betadeltaiota -> Reductionops.nf_all
Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta
Reductionops.whd_betadeltaiota -> Reductionops.whd_all
Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet
Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack
Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack
Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack
Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state
Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state
Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state
Reductionops.whd_eta -> Reductionops.shrink_eta
Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all
Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all
And removed the following ones:
Reductionops.whd_betaetalet
Reductionops.whd_betaetalet_stack
Reductionops.whd_betaetalet_state
Reductionops.whd_betadeltaeta_stack
Reductionops.whd_betadeltaeta_state
Reductionops.whd_betadeltaeta
Reductionops.whd_betadeltaiotaeta_stack
Reductionops.whd_betadeltaiotaeta_state
Reductionops.whd_betadeltaiotaeta
They were unused and having some reduction functions perform eta is confusing
as whd_all and nf_all don't do it.
|
| | |
| |
| |
| |
| |
| |
| | |
Unset Program Generalized Coercion to avoid coercion of general
applications.
Unset Program Cases to deactivate generation equalities and
disequalities of cases.
|
| | |
| |
| |
| |
| | |
For better error messages. The API change is
backwards compatible, using a new optional argument.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
On the user side, coqtop and coqc take a list of warning names or categories
after -w. No prefix means activate the warning, a "-" prefix means deactivate
it, and "+" means turn the warning into an error. Special categories include
"all", and "default" which contains the warnings enabled by default.
We also provide a vernacular Set Warnings which takes the same flags as argument.
Note that coqc now prints warnings.
The name and category of a warning are printed with the warning itself.
On the developer side, Feedback.msg_warning is still accessible, but the
recommended way to print a warning is in two steps:
1) create it by:
let warn_my_warning =
CWarnings.create ~name:"my-warning" ~category:"my-category"
(fun args -> Pp.strbrk ...)
2) print it by:
warn_my_warning args
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
By default obligations defined by tactics are defined
transparently or opaque according to the Obligations Transparent flag,
except proofs of subset obligations which are treated
as opaque by default. When the user proves the obligation using
Qed or Defined, this information takes precedence, and only
when the obligation cannot be Qed'ed because it contains
references to a recursive function an error is raised
(this prevents the guardness checker error).
Shrinked obligations were not doings this correctly.
Forcing transparency due to fixpoint prototypes
takes precedence over the user preference.
Program: do not force opacity of subset proofs,
maintaining compatibility.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When typing a "with clause fails, type classes are used to possibly
help to insert coercions. If this heuristic fails, do not consider it
anymore to be the best failure since it has made type classes choices
which may be inconsistent with other constraints and on which no
backtracking is possible anymore (see new example in test suite file
4782.v).
This does not mean that using type classes at this point is good. It
may find an instance which help to find a coercion, but which might
still be a choice of instance and coercion which is incompatible with
other constraints.
I tend to think that a convenient way to go to deal with the absence
of backtracking in inserting coercions would be to have special
For the record, here is a some comments of what happens regarding
f9695eb4b and 827663982.
In the presence of an instance (x:=t) given in a "with" clause, with
t:T, and x expected of type T', the situation is the following:
Before f9695eb4b:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is postponed to w_merge, even though there is no way to get more
information since T ant T' are closed. As a result, t may be
ill-typed and the unification may try to unify ill-formed terms,
leading to #4872.
- If T and T' are not closed and contains evars of type a type class,
inference of type classes is tried. If it fails, e.g. because a
wrong type class instance is found, it was postponed to w_merge as
above, and the test for coercion is retried now interleaved with
type classes.
After f9695eb4b and 827663982e:
- If T and T' are closed and T <= T' is not satisfiable (no coercion
or not convertible), the test for possible insertion of a coercion
is an immediate failure. This fixes #4872.
- However, If T and T' are not closed and contains evars of type a
type class, inference of type classes is tried. If it gives closed
terms and fails, this is immediate failure without backtracking on
type classes, resulting in the problem added here to file 4872.v.
The current fix does not consider the result of the use of type
classes while trying to insert a coercion to be the last word on
it. So, it fails with an error which is not the error for conversion
of closed terms (ConversionFailed), therefore in a way expected by
f9695eb4b and 827663982e, and the "with" typing problem is then
postponed again.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
We unify types of let-ins in FO heuristic before their bodies, using
cumulativity in either direction. This maintains the invariant that we
are comparing terms in related types throughout unification.
Also adapt test-suite file for bug #3929.
|
| | |
| |
| |
| |
| | |
This allows a smooth addition of various unsafe flags without wreaking
havoc in the ML codebase.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.
Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
This fixes the declarations of constraints, universes
and assumptions:
- global constraints can refer to global universes only,
- polymorphic universes, constraints and assumptions can only be
declared inside sections, when all the section's
variables/universes are polymorphic as well.
- monomorphic assumptions may only be declared in section contexts
which are not parameterized by polymorphic universes/assumptions.
Add fix for part 1 of bug #4816
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
This avoids postponing constraints which will surely produce
an occur-check and allow to backtrack on first-order unifications
producing those constraints directly (e.g. to apply eta).
(fixes HoTT/HoTT with 8.5).
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Function default_fail was always part of an ise_try. Its associated
error message was anyway thrown away. It is then irrelevant and could
be made simpler.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This can happen with the "with" clause (see e.g. #4782), but also with
recursive calls in first-order unification (e.g. "?n a a b = f a" when
a matching between "b" and "a" is tried before expanding f).
|
Pierre-Marie Pédrot
Hugo Herbelin
Emilio Jesus Gallego Arias
Guillaume Melquiond
Matthieu Sozeau
Maxime Dénès
Pierre Letouzey
Matthieu Sozeau
Arnaud Spiwack