| Commit message (Collapse) | Author | Age |
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15916 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15872 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This instance of gen_tactic_expr was used only to decorate
tactics via Refiner.abstract_tactics and alii, but these
expressions are now ignored by the new proof-engine (no "info"...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15865 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15864 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Btw, remove unused code in the xml plugin and in Tactic_printer
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Nested was never constructed, while the notion of abstract_tactic_box
is obsolete (cf. Refiner.abstract_tactic).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15862 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15846 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 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
|
|
|
|
|
|
|
|
|
| |
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
especially about unused definitions, unused opens and unused rec
flags.
The following patch uses information gathered using these warnings to
clean Coq source tree. In this patch, I focused on warnings whose fix
are very unlikely to introduce bugs.
(a) "unused rec flags". They cannot change the semantics of the program
but only allow the inliner to do a better job.
(b) "unused type definitions". I only removed type definitions that were
given to functors that do not require them. Some type definitions were
used as documentation to obtain better error messages, but were not
ascribed to any definition. I superficially mentioned them in one
arbitrary chosen definition to remove the warning. This is unaesthetic
but I did not find a better way.
(c) "unused for loop index". The following idiom of imperative
programming is used at several places: "for i = 1 to n do
that_side_effect () done". I replaced "i" with "_i" to remove the
warning... but, there is a combinator named "Util.repeat" that
would only cost us a function call while improving readibility.
Should'nt we use it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15797 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
Semantic changes are :
- whd_nored_stack remplaces a defined meta by its value whereas the old whd_stack
didn't.
- Zcase and Zfix are alwais put on stack. iota_flag is checked by constructors and
cofix.
- simpl uses its own whd_ function that do not touch at matched term
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15634 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
All the purely monadic code has been moved to a new module Monads,
where, I'm afraid to confess, I got to use a number of proof transformers
to modularise the definition of tactics. It is still not easy to understand (why
would it with backtracking support?) but at least it's more robust, cleaner,
and more extensible. Plus there is now a Proofview.tclORELSE which will
be used to interprete the Ltac tactical (t1 || t2).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15596 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15577 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
| |
If you are focused on 3 subgoals, and unfocusing would reveal 2 extra
subgoals, and unfocusing again would reveal 4 extra subgoals, then coqtop
will tell you:
3 focused subgoals (unfocused: 2-4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15508 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@15418 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 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@15407 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@15392 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
grammar.cma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15384 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
Stuff about reductions now in genredexpr.mli, operations in redops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15374 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
NB: former Tacexpr.no_move is now Tacexpr.MoveLast
(when introducing, intro with no move is intro as last)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
Corresponding operations in locusops.ml and miscops.ml
The type of occurrences is now a clear algebraic one instead of
a bool*list hard to understand.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15372 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15371 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15369 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15202 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
not fully unfocused (in the style of the Guarded command).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15104 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
To mitigate the lack of a general "info" tactical, let's
introduce some specialized tactics info_trivial, info_auto
and info_eauto that display the basic tactics used when
solving a goal.
We also add tactics "debug trivial" and "debug auto" which
display every basic tactics attempted by trivial or auto.
Triggering the "info" or "debug" mode for auto, eauto, trivial
can also be done now via global options, such as Set Debug Auto
or Set Info Eauto. In case both debug and info modes are
activated, the debug mode takes precedence.
NB: it would be nice to name these tactics "info xxx" instead
of "info_xxx", but I don't see how to implement a "info eauto"
in eauto.ml4 (hence by TACTIC EXTEND) while keeping
a generic "info foo" tactic in g_ltac.ml4 (useful to display
a nice message about the unavailability of the general info).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15103 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
No grammar entries for these tactics since coq 8.0
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15102 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
|
|
|
|
|
|
|
| |
There're not compatible with the current Backtrack mecanism used
both by ProofGeneral and CoqIDE.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15083 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
It seems that we can currently do a successful Undo (but not two!)
on a freshly started Lemma. Let's add a depth check on Pfedit.undo
to avoid that. This way, we cannot Undo to depth < 1 (with 1 being
the initial depth of a lemma).
Simplier implementation of Pfedit.restart : it is Pfedit.undo_todepth 1.
This extra initial step in the Undo Stack has probably something
to see with the Lemma argument introduction. For instance, before this
patch we had:
Lemma test n : n+0=n.
Restart. (* now the goal is universally quantified ! *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15075 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
by default typeclass resolution is not launched on goal evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15074 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
| |
i.e.: after a brace is open, one can use the bullets again without clashing with
bullets outside the brace. In particular, one can nest bullets with arbitrary
depth (by interleaving them with occasional braces).
Also fixed a typo introduced in my previous commit which caused bullets
and braces to behave just like regular focuses.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15073 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The optimisation done of Namegen.visibly_occur_id did not preserve
the previous behavior when pr_constr/constr_extern/detype were
called on a term with free rel variables. We backtrack on it to
go back to the 8.2 behavior.
Seized this opportunity to clarify the meaning of the at_top flag
in constrextern.ml and printer.ml and to rename it into
goal_concl_style. The badly-named at_top flag was introduced in
Coq 6.3 in 1999 to mean that when printing variables bound in the
goal, names had to avoid the names of the variables of the goal
context, so as to keep naming stable when using "intro"; in
r4458, printing improved by not avoiding names that were short
names of global definitions, e.g. "S", or "O" (except when the
at_top flag was on for compatibility reasons).
Other printing strategies could be possible in the
non-goal-concl-style mode. For instance, all bound variables
could be made distinct in a given expression, even if no clash
occur, therefore following so-called Barendregt's
convention. This could be done by setting "avoid"
to "ids_of_rel_context (rel_context env)" in extern_constr and
extern_type (and then, Namegen.visibly_occur_id could be
re-simplified again!).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15067 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
of evars.
Used when interpreting a constr in Ltac: resolution is now launched if the constr
is casted.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15038 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
toplevel/
The code is not called yet from there.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15033 85f007b7-540e-0410-9357-904b9bb8a0f7
|