| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
If a goal is given and wrong, exception is raised. If no goal is
given, then goal 1 is tried but no failure if goal 1 does not exist,
just fall back to gloab env.
|
|
|
|
|
| |
Patch by CJ on bugzilla. CUnix.sys_command doesn't rely on a shell, so extra
care with cmd.exe vs sh is no longer required.
|
|
|
|
|
| |
Since it displays together with the goal, it is better (for pg and
other interfaces probably) that they are in a different message.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
step, prefer QuestionMark's to other evars, to comply with the
filtering made on VarInstance, GoalEvar and QuestionMark for type
class resolution. Maybe evars to be resolved by type class instances
should eventually be marked with a specific tag.
At least, this solves the current problem with compiling cancel2.v in
LemmaOverloading.
|
|
|
|
|
|
|
| |
+ consequences of this check on the standard library (moved the no-op
in Notation modifiers to what there were supposed to do; these are
anyway local notations, so compatibility is safe - please AS or PL,
amend if needed).
|
|
|
|
| |
unification flags (see also temporary revert in d083200ae5b).
|
| |
|
| |
|
| |
|
|
|
|
| |
twice). Thanks to Marc Lasson for spotting this.
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
This reverts commit ad2a0308b1592c7235714a2cca926f3b55accbb2.
|
|
|
|
| |
[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.
|
|
|
|
|
|
|
| |
for typeclasses.
This was not the case for goals created at the end of the tactic by salvaging the [future_goals] from the evar map. It would cause typeclass resolution to try and solve these goals (if they have a class type) at each subsequent tactic.
Fixes #3841.
|
|
|
|
|
|
|
|
|
|
|
| |
This makes such things work:
x:nat
h: x = 3
================
True
Search x.
|
| |
|
| |
|
| |
|
| |
|
|
|
|
| |
You can write 'simpl -[plus minus] div2'. Simpl does not use it for now.
|
|
|
|
| |
Documentation also updated.
|
|
|
|
|
|
|
|
| |
- In evarconv, check_conv_record properly computes the parameters of
primitive record projections for later unification, adding env and
sigma as arguments.
- In unification, backtrack on pattern-unification and not only
application unification if eta for a record failed.
|
|
|
|
| |
redex.
|
| |
|
| |
|
| |
|
|
|
|
|
|
| |
Revert "Fixing an evar_map bug revealed by commit 603b66f81 on unification flags."
This reverts commit d083200ae5b391ceffaa0329a8e3a334036c7968.
|
|
|
|
| |
in reporting the chain of causes when unification fails.
|
| |
|
|
|
|
| |
pattern-matching predicate.
|
|
|
|
| |
This fixes current failure of RelationAlgebra.
|
| |
|
| |
|
| |
|
|
|
|
| |
is not defined while X_rect is, for example in HoTT/Coq.
|
|
|
|
| |
kernel reduction.
|
|
|
|
|
|
|
|
|
|
|
| |
In the case of conversion, postponing by preserving the
initial orientation.
Was wrong from its initial version in Jan 2014, but was not visible
because evar-evar subtyping was approximated by evar-evar conversion.
Thanks to Enrico for a very short example highlighting the problem. In
particular, this fixes Ergo.
|
|
|
|
|
|
| |
test pattern-unification after restriction of the evars so as to
succeed earlier (no observational changes however in the examples at my
disposal).
|
| |
|
| |
|
|
|
|
| |
e.g. for MTac.
|
| |
|
|
|
|
|
|
| |
Putting utf8 everywhere helps the maintainance of the online refman.
And anyway, this is the way to go. We should also chase and migrate
the few remaining iso-latin-1 files elsewhere in the sources.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Unfortunately, these ?uri=referer parameters do not work correctly
now that coq.inria.fr forces the switch to https before answering
any document. See: http://validator.w3.org/docs/help.html#faq-referer
I currently see no workaround for that, apart from generating links
like ?uri=http://the.real.url/of/my/page, which would be quite painful.
For now, users interested in checking the validity of our pages
will have to copy-paste the url they want to check after clicking
on the validator button.
|