| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
Some asynchronous constraints between initial universes and the ones at
the end of a proof were forgotten. Also add a message to print universes
indicating if all the constraints are processed already or not.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Internal error: Anomaly: Uncaught exception Not_found. Please report.
An evarmap was lost because of an unsound typing primitive.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some functions from pretyping/typing.ml and their derivatives were potential
source of evarmap leaks, as they dropped their resulting evarmap. This commit
clarifies the situation by renaming them according to a unsafe_* scheme. Their
sound variant is likewise renamed to their old name. The following renamings
were made.
- Typing.type_of -> unsafe_type_of
- Typing.e_type_of -> type_of
- A new e_type_of function that matches the e_ prefix policy
- Tacmach.pf_type_of -> pf_unsafe_type_of
- A new safe pf_type_of function.
All uses of unsafe_* functions should be eventually eliminated.
|
| |
|
|
|
|
|
|
|
|
|
| |
It accepts three distinct flags:
- "Lax", which is the default one, sets the old behaviour, i.e. a non-imported
hint behaves the same as an imported one.
- "Warn" outputs a warning when a non-imported hint is used. Note that this is
an over-approximation, because a hint may be triggered by an eauto run that
will eventually fail and backtrack.
- "Strict" changes the behaviour of an unloaded hint to the one of the fail
tactic, allowing to emulate the hopefully future import-scoped hint mechanism.
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
We beta-iota normalize the type of the rewriting predicate to ensure that the
non-dependency in the arrow argument is meaningful. Otherwise, terms of the
form "forall x : A, (fun _ : A => P) x" generated by the retyping would confuse
the non-dependency heuristic.
|
| | |
|
| |
|
|
| |
preserving compatibility of subst after #4214 being solved.
|
| |
|
|
|
|
| |
Improving treatment of recursive equations compared to 8.4 (see test-suite).
Experimenting not to unfold local defs ever in subst.
(+ Slight simplification in checking reflexive equalities only once).
|
| |
|
|
|
| |
after patch for #4214 on subst needed to be repeated (see
857e82b2ca0d1).
|
| |
|
|
|
| |
The hypinfo cache was actually always set to None, so that there was no need
to try to preserve it if it was set to an actual value.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
equalities in configurations like
x=y
x=z
===
P(x,y,z)
where it now produces
===
P(z,z,z)
In particular (equations are processed from most ancient to most recent).
Thanks to this, a "repeat subst" can just be a "subst" in List.v.
Incidentally: moved a nf_enter to enter in subst_one, since the latter
is normally called from other tactics having normalized evars.
|
| | |
|
| |
|
|
|
|
| |
Since error messages are ultimately passed to Format, which has its own
buffers for concatenating strings, using concatenation for preparing error
messages just doubles the workload and increases memory pressure.
|
| | |
|
| |
|
|
|
| |
Followup of: f7b29094fe7cc13ea475447bd30d9a8b942f0fef . In particular, re-closes #3593.
As a side effect, fixes an undiscovered bug of the `eq_constr` tactic which didn't consider terms up to evar instantiation.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
We provide an eliminator ensuring that the AST will be used to build a tactic,
so that we can stuff arbitrary things inside. An escape function is also provided
for backward compatibility.
|
| |
|
|
| |
the context... overlooked by my last commit. Fixes relation-algebra.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
Btw, also unset the READABLE_ML4 option, which probably caused
this issue. No, we normally do *not* want to see the internals
of .ml generated out of a .ml4 (except during some specific debug
sessions). It is *so* easy otherwise to edit the wrong .ml by
mistake and forget to edit the original .ml4.
|
| |
|
|
|
|
| |
takes a variable substitution for matched variables in the (lhs) pattern, and
uses the existing ist structure to pretype the rhs correcly, without
having to deal with the volatile evars.
|
| |
|
|
|
|
|
|
| |
This patch changes the semantics of eauto w.r.t. to extern hints, so it may
break some code out there. There is no compatibility flag because this is a
real bug, and we do not really want the users to depend on this. Moreover, there
are still some fishy parts in the current implementation that should be rewritten
for the next release.
|
| |
|
|
|
|
| |
They are all generated by the Hints module, and making them purely opaque is
not worthwhile because we project them a lot. This ensures that they all get
generated following a uniform process.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Meta variables in rewrite rules are named by integers that are allocated
sequentially at runtime (fresh_meta in tactics/term_dnet.ml). This causes
a problem when some rewrite rules (with meta variables) are generated by
coqc, saved in a .vo file, and then imported into another coqc/coqtop
process. The new process will allocate its own meta variable numbers
starting from 0, colliding with existing imported meta variable numbers.
One manifestation of this issue was various failures of [rewrite_strat];
see bug #3815 for examples.
This change fixes the problem, by replacing all meta variable numbers
in imported rewrite rules at import time. This seems to fix the various
failures reported in bug #3815.
Thanks to Jason Gross for tracking down the commit that introduced this
bug in the first place (71a9b7f2).
|
| |
|
|
|
| |
Also removed the require function it was using, as it is absent from the
remaining of the code.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- no more inconsistent Axiom in the Prelude
- STM can now process Admitted proofs asynchronously
- the quick chain can stock "Admitted" jobs in .vio files
- the vio2vo step checks the jobs but does not stock the result
in the opaque tables (they have no slot)
- Admitted emits a warning if the proof is complete
- Admitted uses the (partial) proof term to infer section variables
used (if not given with Proof using), like for Qed
- test-suite: extra line Require TestSuite.admit to each file making
use of admit
- test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to
find TestSuite.admit
|
| |
|
|
| |
seem to be overly strong in practice (see discussion related to #4035).
|
| |
|
|
|
| |
Not inventing a new fresh name if a non-fresh name is explicitly
given, as in v8.4.
|
| |
|
|
|
|
| |
pattern_of_constr in an evar_map, as they can appear in the context
of said named metas, which is used by change. Not sure what to do in
the PEvar case, which never matches anyway according to Constr_matching.matches.
|
| | |
|
| |
|
|
| |
inductive type with let-in in the arity (until logic.ml disappears).
|
| |
|
|
|
|
| |
The notations using tactics in term seem now not to respect globalized names.
It is not obvious that this is the expected behaviour, but at least it does
not die with an anomaly.
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
Since they don't work anymore.
|
| | |
|
| | |
|
| | |
|
| | |
|
Matthieu Sozeau
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Arnaud Spiwack
Matthieu Sozeau
Pierre Letouzey
Nickolai Zeldovich
Enrico Tassi