| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
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.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
When setoid rewriting in a hypothesis, we push the newly introduced declaration
after the last declaration it depends on.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
| |
This reverts commit 36c7fba1180eaa2ceea7cc486ebd2f0d649042f0.
I had mixed up the boolean flag, resulting in the loss of evar-free
versions of tactics.
|
| | |
|
| |
|
|
|
|
|
| |
Argument" which I used temporarily in a branch to have "destruct eq_dec"
working like in v8.4 and not like the "destruct (eq_dec _ _)"
of 8.4. I finally made "destruct (eq_dec _ _)" working in 8.5 like
"destruct eq_dec" was working in 8.4 (and is still working in 8.5).
|
| |
|
|
| |
Ultimately setoid rewrite should be written in the monad to fix it properly.
|
| |
|
|
| |
printing functions touched in the kernel).
|
| |
|
|
|
| |
One remaining issue: aliased constants raise an anomaly when some unsubstituted
universe variables remain. VM may suffer from the same problem.
|
| |
|
|
|
|
| |
Not supposed to be part of 8.5beta.
This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
|
| |
|
|
|
| |
respect dependencies between typeclass goals, trying to solve the least
dependent ones first.
|
| |
|
|
|
|
| |
Off by default as it can be backwards-incompatible (e.g. produces
loop in the library without an additional Typeclasses Opaque directive
in RelationPairs).
|
| |
|
|
|
| |
in typeclasses eauto, remaining compatible with eauto and still
producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
|
| | |
|
| | |
|
| | |
|
| |
|
| |
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].
|
| | |
|
| |
|
|
|
|
| |
there is no focused goal.
The 'g' is for "global". The arguments are the same as [fail]. Beware: [let x := constr:… in tac] is a goal-local operation regardless of whether [tac] is goal-local or not.
|
| | |
|
| |
|
|
|
|
| |
This was due to the unqualified uses of "Lazy" being disambiguated in different manners. I just changed the constructor name to "Select".
Fixes #3877.
|
| |
|
|
| |
[multimatch … with …] returns every possible successes: every matching branch and every successes of these matching branch, so that subsequent tactics can backtrack as well.
|
| |
|
|
|
| |
I added a emacs_logger.
Still need to cleanup std_logger.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
[tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
|
| |
|
|
| |
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
| |
|
|
| |
redex.
|
| |
|
|
| |
pattern-matching predicate.
|
| |
|
|
| |
is not defined while X_rect is, for example in HoTT/Coq.
|
| | |
|
| |
|
|
|
|
|
| |
As their commit messages suggested it, these commits were not intended
to be committed at this time. They are part of a on-going merge of the
code of induction and functional induction. Together with the fix
here, they are supposingly transparent, semantically speaking.
|
Pierre-Marie Pédrot
Hugo Herbelin
Arnaud Spiwack
Guillaume Melquiond
Matthieu Sozeau
Matthieu Sozeau
Matěj Grabovský
Maxime Dénès
Pierre Courtieu
Pierre Letouzey