| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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.
|
|
|
|
|
|
|
|
Commit 84c2433a introduced the Any type alias as the Haskell extracted
version of MiniML's Tunknown. However, the code to define the Any
type alias was generated conditional on usf.magic. As it turns out,
sometimes Tunknown appears even if usf.magic is false (i.e., even if
MLmagic does not appear anywhere in the AST). This produced Haskell
code that would not compile; e.g.:
% coqtop
Coq < Extraction Language Haskell.
Coq < Extraction Library Datatypes.
The file Datatypes.hs has been created by extraction.
% ghc Datatypes.hs
[1 of 1] Compiling Datatypes ( Datatypes.hs, Datatypes.o )
Datatypes.hs:261:17: Not in scope: type constructor or class `Any'
Datatypes.hs:261:24: Not in scope: type constructor or class `Any'
The fix is straightforward: produce the code that defines the Any type
alias if usf.tunknown is true.
|
|
|
|
No "read-only" terminator. If no terminator is present the UI
complains. If the terminator is different, STM warns but
continues. The STM warns that the "check the document" button
will not honor the terminator change, and what to do to avoid
that.
Technically, one cannot turn (a posteriori) an axiom into a theorem
and vice versa. Could be done, but not with a small patch.
|
|
|
|
subdirectories.
Using Mltop.add_path instead of Mltop.add_rec_path causes the following
kind of behavior:
$ coqtop -nois
Coq < Require Import Coq.Init.Datatypes.
Error: Cannot find a physical path bound to logical path Coq.Init.
The only case where its use is still warranted is the implicit "." path. It
shall not be recursive because Coq might be called from about anywhere.
This patch also removes -I-as since its behavior is no longer the one from
8.4 so it is not worth keeping it around.
|
|
"Add LoadPath" is documented as acting as -Q, not as -I-as. Note that
"Add Rec LoadPath" should be used when compatibility with 8.4 matters.
|
|
|
|
Without this commit, passing "-R theories Coq" to "coqtop -nois" has no
effect since "-Q theories Coq" has already been done implicitly.
|
|
|
|
|
|
|
|
|
|
Most of them are backports of improvements already there in
FSetPositive when compared with the original FMapPositive file.
|
|
replacement for 8.4's "Require Omega").
|
