| Age | Commit message (Collapse) | Author |
|---|
|
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").
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also removed the require function it was using, as it is absent from the
remaining of the code.
|
|
|
|
|
|
|
|
The new behaviour is simple: either a path is in the loadpaths or it is not.
No more wild expansions of paths!
This should not affect -R and -Q, but it does change the semantics of -I -as.
Still, there are no more users of it and it only does so in a subtle way.
|
|
`end proof` changes the proof mode to `"Classic"`.
|
|
So that the commands are assigned the appropriate status of syntax-changing or not, as well as the proof mode they are setting.
|
|
It will not work in CoqIDE though, which handles printing its own way. It's a general remark that we have many ways of printing things in Coq and we should look for a unified structured framework to be shared between interfaces.
|
|
|
|
This is meant to help integrate the printers of the declarative mode.
|
|
Closes #57.
|
|
|
|
|
|
This is necessary to make ssr compile with both camlp4/5
|
|
|
|
|
|
|
|
|
|
|
|
The context matching function was dropping the surrounding context in
let-ins.
|
|
Note that I do not understand why the delimiter map is incomplete on
loading and thus was causing a failure. So, while the patch is the proper
way to deal with notation scopes, there might be another bug lurking in
this file.
|
|
|
|
When a worker sends back a system state to master, it tries to
just send a delta. If the command is a simple tactic, then only
the proof state changes.
Now, what is a simple tactic?
1. a tactic
2. that does not change the environment
Check 1. was surely incomplete. Now it is:
VernacSolve _ | VernacFocus _ | VernacUnfocus | VernacBullet _
Is it complete?
|
|
|
|
for which there corresponding tag are greater than max_variant_tag.
The code is a merge with the patch proposed by Bruno on
github barras/coq
commit/504c753d7bb104ff4453fa0ede21c870ae2bb00c
|
