| Age | Commit message (Collapse) | Author |
|---|
|
|
|
When setoid rewriting in a hypothesis, we push the newly introduced declaration
after the last declaration it depends on.
|
|
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
|
|
|
Because of f66b84de608830600e43f6d1a97c29226b6b58ea (Refine primitive: [unsafe] is now true by default), setoid rewrite could produce ill-typed term. Since setoid rewrite relies on the checks of refine to ensure well-typed, turned the check explicitely on with [~unsafe:false].
|
|
Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.
To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.
The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.
|
|
normalize it afterwards.
|
|
In particular, the old hypinfo is made as a proper cache, preventing dynamic
tricks to decide whether it was rightful to refresh it.
|
|
This allows to have the example in test setoid_unif.v to work again.
|
|
|
|
- removed the encapsulation in a Tactic Failure (I don't see why
setoid_rewrite should specifically raise a Fail - do I miss something?)
- avoid having twice a "Unable to satisfy ... constraints" message.
|
|
of the function are dependent.
|
|
|
|
|
|
Observing that systematic eager evar unification makes unification
works better, for instance in setoid rewrite (ATBR, SemiRing.v), we
add a new flag use_evars_eagerly_in_conv_on_closed_terms which is put
to true only in Rewrite.rewrite_core_unif_flags (empirically, this
makes the "rewrite" from rewrite.ml working again on examples which
were previously treated by use_metas_eagerly_in_conv_on_closed_terms).
|
|
|
|
|
|
an updated evar_map, as pattern is working up to universe equalities
that must be kept. Straightforward adaptation of the code depending on
this.
|
|
|
|
The Unsafe module is for unsafe tactics which cannot be done without anytime soon. Whereas V82 indicates a function which we want to get rid of and that shouldn't be used in a new function.
|
|
As simple as this looks, there's been some quite subtle issues in doing this modification, there may be bugs left.
|
|
|
|
|
|
The old implementation did not beta-iota normalize before observing the head of
the term, resulting in stange bugs.
|
|
|
|
Now, usual function from Evarutil are used to define evars instead of the variants from Proofview.Refine.
The [update] primitive which tried to patch the difference between pretyping functions and the refine primitive is now replaced by the identity function.
|
|
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
|
|
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
|
|
This code was wrong but luckily unused. It instantiated an evar with an
instance where the let-in bindings were removed.
|
|
will name the goal id; writing ?[?id] will use the first
fresh name available based with prefix id.
Tactics intro, rename, change, ... from logic.ml now preserve goal
name; cut preserves goal name on its main premise.
|
|
under binders. This might incur a significant time penalty.
|
|
two versions of the rewriting lemma, keeping useless evars around. This
can now happen only when the rewrite lemma is used under binders... Fix
to do next.
|
|
This removes a use of Evd.merge.
|
|
The hypinfo state is now refreshed at a proper time, which should reduce the
overall number of calls to [decompose_applied_relation]. The state passing
nature of the program is also more explicit, removing a use of Evd.merge.
This patch should preserve semantics and efficiency.
|
|
|
|
|
|
Add a global option to check for multiple solutions and fail in that
case.
Add another flag to declare classes as having unique instances (not
checked but assumed correct, avoiding some backtracking).
|
|
|
|
|
|
|
|
the abs flag in rewrite.
|
|
|
|
|
|
|
|
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
|
|
|
|
selection (rewrite, destruct/induction, set or apply on scheme), for
unification (apply on not a scheme, auto), the latter being separated
into primary unification and unification for merging instances.
No change of semantics from within Coq, if I did not mistake (but a
function like secondOrderAbstraction does not set flags by itself
anymore).
|
|
1. Proofview.Goal.enter into Proofview.Goal.nf_enter.
2. Proofview.Goal.raw_enter into Proofview.Goal.enter.
3. Proofview.Goal.goals -> Proofview.Goals.nf_goals
4. Proofview.Goal.raw_goals -> Proofview.Goals.goals
5. Ftactic.goals -> Ftactic.nf_goals
6. Ftactic.raw_goals -> Ftactic.goals
This is more uniform with the other functions of Coq.
|
|
|
|
|
