| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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.
|
|
|
|
This is important to disambiguate identical names from different modules.
|
|
This patch allows Coq terms to be extracted into the widely used JSON
format. This is useful in at least two cases:
- One might want to manipulate Coq values outside of Coq, but without
being forced to use one of the three existing extraction languages
(OCaml, Haskell, or Scheme), and without having to compile Coq's
extracted result. This is especially useful when a Coq evaluation
produces some data structure that needs to be moved out of Coq.
Having to invoke an OCaml/Haskell/Scheme compiler just to get a
data structure out of Coq is somewhat awkward.
- One might want to experiment with extracting Coq code into other
languages (Go, Javascript, etc), without having to write the whole
extraction logic in OCaml and recompile Coq's extraction plugin
each time. This makes it easy to quickly prototype extraction
in any language, without having to build Coq from source.
Extraction to JSON is implemented by adding the JSON "pseudo-language"
to the extraction facility. Thus, one can extract the JSON encoding
of a single term using:
Extraction Language JSON.
Extraction qualid.
and extract an entire Coq library "ident" into "ident.json" using:
Extraction Language JSON.
Extraction Library ident.
Nota (Pierre Letouzey) : this is an updated version of the original
PullRequest, updated to match recent changes in trunk
|
|
spurious quantification on unused universes.
|
|
|
|
|
|
The extraction machinery has specialized support for extracting [ascii]
characters into native characters in the target language, as opposed
to using an explicit constructor from 8 boolean bits. This works by
hard-coding the name of the character type in the target language.
Unfortunately, the hard-coded type for Haskell was "Char", not the
fully-qualified "Prelude.Char". As a result, it was impossible to
extract characters into Haskell without getting type errors about "Char".
This patch changes this hard-coded name to "Prelude.Char".
|
|
|
|
|
|
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).
|
|
The old behavior was extremely annoying, especially when using coqide from
the command line, since the "open" box would then point to a seemingly
random point of the filesystem rather than to the directory of the files
currently being edited (since they were passed on the command line rather
than by point-and-click).
The new behavior matches the one of mainstream editors, e.g. emacs, gedit.
|
|
|
|
|
