| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
States.freeze takes ~marshallable:bool, so that (only) when we want to
marshal data to disk/network we can ask the freeze functions of the
summary to force lazy values. The flag is propagated to Lib and Summary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16478 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This is a no op for standard Coq, but is important for
Paral-ITP, since saving the library to disk forces all
frozen computations, and some of them may spit out glob
data, so the file descriptor must be valid.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
I did forget a ; while dealing with conflicts in git-svn rebase
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16458 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16452 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16444 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16418 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
the interface.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16302 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16294 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
This meta-exception was already almost unused, just to distinguish
exceptions during parsing or interp.
Some code cleanup btw
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16293 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16291 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
Printing Ltac code is broken. This was not compiling with -time
Ltac pop_succn e := eval lazy beta iota delta [plus] in (1 + 1).
The bug in the pretty printer should be fixed too...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16262 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
Ok, this is merely a matter of taste, but up to now the usage
in Coq is rather to use capital letters instead of _ in the
names of inner modules.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16221 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
mechanism to retrieve the same information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
I hope I did not forget some [with] clauses. Otherwise, some
stack frame will be missing from the debug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16167 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16072 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16005 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Util module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15802 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
compiler warnings).
I was afraid that such a brutal refactoring breaks some obscure
invariant about linking order and side-effects but the standard
library still compiles.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Currently :
- only Admitted uses the Unsafe return status
- the status is ignored in coqtop
- Coqide sees the status but apparently doesn't use it for colouring (I'm not
sure why, but then again, it's not as if I understood coqide's code or
anything)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15610 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This provides an ad-hoc way to solve the second part of
bug #2820 (Show Script not working when proof started inside a Load)
When doing Load on a file, two behaviors are possible:
- either the history stack is grown by only one command,
the "Load" itself. This is mandatory for command-counting
interfaces (CoqIDE).
- either each individual sub-commands in the file is added
to the history stack. This allows commands like Show Script
to work across the loaded file boundary (cf. bug #2820).
Ideally, we should be able to combine someday the benefits of
the two approaches. But in the meantime, we resort to a flag :
using "Unset Atomic Load" should make "Show Script" work across Load.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15599 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
This was a wish by A. Chlipala on coq-club
Both Reset foo and Reset Initial are accepted (with a warning).
If some proofs were opened, all of them are aborted. This isn't the
behavior of the interactive Reset that has more information and can
be more selective, but this shouldn't be a big issue in practice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15597 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15481 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
were closed (i.e. the only remaining ones are those of printing/parsing).
Meanwhile, a simplified interface is provided in loc.mli.
This also permits to put Pp in Clib, because it does not depend on
CAMLP4/5 anymore.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15475 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15415 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15394 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Adds a directory ./intf for pure interfaces.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15367 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15219 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- Clib that does not depend on camlpX and is made to be shared by all coq
tools/scripts/...
- Lib that is Coqtop specific
As a side effect for the build system :
- Coq_config is in Clib and does not appears in makefiles
- only the BEST version of coqc and coqmktop is made
- ocamlbuild build system fails latter but is still broken
(ocamldebug finds automatically Unix but not Str. I've probably done something wrong here.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15144 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Migrate the backtracking code from ide_slave.ml into a new backtrack.ml.
In particular the history stack of commands that used to be there is now
non-coqide-specific.
** Adapted commands **
- "Show Script": a basic functional version is restored (and the printing
of scripts at Qed in coqtop). No indentation, one Coq command per line,
based on the vernac_expr asts recorded in the history stack, printed via
Ppvernac.
- "Back n" : now mimics the backtrack of coqide: it goes n steps back
(both commands and proofs), and maybe more if needed to avoid re-entering
a proof (it outputs a warning in this case).
- "BackTo n" : still try to go back to state n, but it also handles the
proof state, and it may end on some state n' <= n if needed to avoid
re-entering a proof. Ideally, it could someday be used by ProofGeneral
instead of the complex Backtrack command.
** Compatible commands **
- "Backtrack" is left intact from compatibility with current ProofGeneral.
We simply re-synchronize the command history stack after each Backtrack.
- "Undo" is kept as a standard command, not a backtracking one, a bit like
"Focus". Same for "Restart" and "Abort". All of these are now accepted
in coqide (Undo simply triggers a warning).
- Undocumented command "Undo To n" (counting from start of proof instead of
from end) also keep its semantics, it is simply made compatible with
the new stack mechanism.
** New restrictions **
We now forbid backtracking commands (Reset* / Back*) inside files
when Load'ing or compiling, or inside VernacList/VernacTime/VernacFail.
Too much work dealing with these situation that nobody uses.
** Internal details **
Internally, the command stack differs a bit from what was in Ide_slave
earlier (which was inspired by lisp code in ProofGeneral). We now tag
commands that are unreachable by a backtrack, due to some proof being
finished, aborted, restarted, or partly Undo'ed. This induce a bit of
bookkeeping during Qed/Abort/Restart/Undo, but then the backtracking code
is straightforward: we simply search backward the first reachable state
starting from the desired place. We don't depend anymore on the proof
names (apart in the last proof block), It's more robust this way
(think of re-entering a M.foo from an outside proof foo).
Many internal clarifications in Lib, Vernac, etc. For instance
"Reset Initial" is now just a BackTo 1, while "Reset foo" now calls
(Lib.label_before_name "foo"), and performs a BackTo to the corresponding
label.
Concerning Coqide, we directly suppress the regular printing of goals
via a flag in Vernacentries. This avoid relying on a classification
of commands in Ide_slave as earlier.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15085 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14945 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
are declared as such, but I suspect Coq to contain some more.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
packages for utf8.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Anomalies are now meant to be the exceptions that are *not*
catched and handled by the new Errors.handle_stack.
Three variants of [Errors.print] allow to customize how anomalies
are treated. In particular, [Errors.print_no_anomaly] is used
for the Fail command, instead of a classification function
Cerrors.is_user_error which wasn't customizable.
No more AnomalyOnError, its only occurrence is now a regular anomaly
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14133 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
For that, I introduce a explicit classification function
is_user_error : exn -> bool, instead of the previous hack
of explain_exn_default_aux (fun () -> raise e).
By the way, clean a bit explain_exn_default_aux : many cases
are just printed fine by default's Printexn.to_string (for example
Not_found).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14129 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13916 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Local/Global modifiers in interpretation loop so as to support
Local/Global for grammar extension) that made use of
DuringSyntaxChecking error wrapper inappropriately nested with the
DuringCommandInterp error wrapper, what disturbed the error
processors. Good thing, we can now simplify things and completely
remove the DuringSyntaxChecking wrapper.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13667 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13583 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
location is raised from a loaded/compiled file!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13488 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
too late, in a global environment which was no longer the correct one,
leading to the failure of error printing (hence an anomaly) in case
the command modified the state in several steps.
Now, errors raised by vernac commands are processed in the same
(intermediate) state they were raised from, just before rolling back
to the original state.
that modify the state in several
Now, errors raised by vernac commands that modify the state in several
steps (say S1, S2, ..., Sn) are processed in the state they were
produced in (S1, S2, ... Sn-1),
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13431 85f007b7-540e-0410-9357-904b9bb8a0f7
|