| Commit message (Collapse) | Author | Age |
|---|
| |
|
| |
Restores the intended behaviour from v8.3 and earlier.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
as glued.
Possible improvement: rotate using the left children in the glue function,
so that the iter function becomes mostly tail-recursive. Drawback: two
allocations per glue instead of a single one.
This commit makes the following command go from 7.9s to 3.0s:
coqtop <<< "Require Import BigZ ZBinary Reals OrdersEx. Time SearchPattern _." | tail -n 1
|
| | |
|
| | |
|
| |
|
|
|
| |
This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
|
| |
|
|
| |
for being able to interpret a "match" as a constr pattern).
|
| |
|
|
| |
in the presence of let-ins).
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
them (e.g. "fun ... ⇒ ...") factor well (see #2268).
|
| |
|
|
| |
We just inline the state in the iolist: less closures makes the GC happier.
|
| | |
|
| |
|
|
| |
libraries at once (see #4193).
|
| | |
|
| |
|
|
|
|
| |
This patch should get rid of the following warning:
Invalid character '-' in identifier "v8-syntax".
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
The solution is a bit ugly. In order for two tactic notations identifiers not
to be confused by the inclusion from two distinct modules, we embed the name of
the source module in the identifiers. This may still fail if the same module is
included twice with two distinct parameters, but this should not be possible
thanks to the fact any definition in there will forbid the inclusion, for it
would be repeated. People including twice the same empty module otherwise
probably deserve whatever will arise from it.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Long story short: Filname.concat and other OCaml provided functions
to be "cross platform" don't work for us for two reasons:
1. their behavior is fixed when one compiles ocaml, not when one runs it
2. the build system of Coq is unix only
What is wrong with 1 is that if one compiles ocaml for windows
without requiring cygwin.dll (a good thing, since you don't need to
have cygwin to run ocaml) then the runtime always uses \
as dir_sep, no matter if you are running ocaml from a cygwin shell.
If you use \ as a dir separaton in cygwin command lines, without
going trough the cygpath "mangler", then things go wrong.
The second point is that the makefiles we have need a unix like
environment (e.g. we call sed). So you can't compile Coq without
cygwin, unless you use a different build system, that is not what
we support (1 build system is enough work already, IMO).
To sum up: Running coq/ocaml requires no cygwin, comipling coq requires
a unix like shell, hence paths shall be unix like in configure/build stuff.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
| |
definition time. The obligation tactic or user can still choose to do so.
|
| |
|
|
| |
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.
|
| | |
|
| |
|
|
| |
instances as definitions and lemmas do (fixes bug# 4121).
|
| | |
|
| |
|
|
|
| |
removing all evars appearing in the constr (or their types,
recursively) from the evar_map.
|
| |
|
|
| |
has a strict upper bound.
|
| |
|
|
| |
QuicksortComplexity).
|
| |
|
|
| |
Since [map_ext_in] is more general, no need to have the same proof twice.
|
| |
|
|
|
|
| |
Slightly broader version of the existing [map_ext]: two [map] expressions
are equal if their respective functions agree on all arguments that are
in the list being mapped.
|
| | |
|
Arnaud Spiwack
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Guillaume Melquiond
Enrico Tassi
Pierre-Marie Pédrot
jforest
Pierre Letouzey
Matthieu Sozeau
Nickolai Zeldovich