| Age | Commit message (Collapse) | Author |
|---|
|
Example: "Implicit Arguments eq_refl [[A] [x]] [[A]]".
This should a priori be used with care (it might be a bit disturbing
seeing the same constant used with apparently incompatible signatures).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13484 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In particular, the unused lib/tlm.ml and lib/gset.ml are removed
In addition, to simplify code, Libobject.record_object returning only the
('a->obj) function, which is enough almost all the time.
Use Libobject.record_object_full if you really need also the (obj->'a).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13460 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
coqide doc link is the canonical link to last released version of
reference manual instead of link to corresponding coqide version).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13436 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- modules names can include quote '
- errors when parsing .mllib files are now properly reported
instead of dying ugly on some sort of Failure
- same when coqdep has to parse the output of ocamldep -modules
- lib/lib.mllib contains a typo (lowercase ident)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13423 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
proofs is now the default behavior of coqtop.
* lib/Coqtop: Update accordingly.
* checker/Check library/Library:
Pass the right "load_proofs" flag to LightenLibrary.load.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13379 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
requiring a file Utf8_core. That needs to be improved...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13358 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
with non-recursive binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13357 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
location dumping for binders uniformly treated in constrintern.ml (and
renamed the optional arg of interp_context from fail_anonymous to
global_level since the flag now also decides whether to dump binders as
global or local ones); added locations for the variables occurring in
the "as in" clauses;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13314 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13298 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Looking at the source code of Sys.time reveals that it is exactly what
is computed by Profile.get_time. This can also be tested by evaluating:
Sys.time () -. Unix.(let x = times () in x.tms_utime +. x.tms_stime);;
in an OCaml toplevel with Unix.
This allows to put Profile in grammar.cma without the dependency to
unix.cma while preprocessing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13233 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
thunks. Move from [lazy] to [delayed] in subtac.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Applied it to fix mli file headers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13175 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
#2158,#2179)
Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is
the hexa code for the unicode index of this character. For instance
<alpha> is turned into __U03b1_. I know, this is ugly. Better
solutions are welcome, but I'm afraid we can't do much better as long
as ocaml and haskell don't accept unicode letters in idents. At
least, this way we're pretty sure this translating won't create name
conflit, as long as extraction users avoid __ in their names,
something that they should already do btw (see for instance
extraction of coinductive types in ocaml). Yes, I should add a test
and a warning/error in case of use of __ someday.
NB: this commit belongs proudly to the quick'n'dirty category
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
people use the undocumented "Lemma foo x : t" feature in a way
incompatible with this activation.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
binders.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13086 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13044 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This commit changes many things in CoqIDE, and several breakage are to
be expected. So far, evaluation in standard tactic mode and backtracking
seems to be working.
Future work :
- clean up the thread management crud remaining in ide/coqide.ml
- rework the exception handling
- rework the init system in Coqtop
plus many other things
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13043 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13035 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Most of the code in search_exe_in_path was about parsing the PATH into a list
of directories, which is now done in function lpath_from_path. Existence of the
file is checked using already existing functions, so that duplication is
minimized.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13033 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Cf tok.ml, token isn't anymore string*string where first
string encodes the kind of the token, but rather a nice
sum type. Unfortunately, string*string (a.k.a Plexing.pattern)
is still used in some places of Camlp5, so there's a few
conversions back and forth. But the penalty should be quite low,
and having nicer tokens helps in the forthcoming integration
of support for camlp4 post 3.10
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13018 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13017 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13016 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Ocaml 3.10.0 is already three year old...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13015 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12976 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dev/ocamlweb-doc has been erased. I hope no one still use the
"new-parse" it generate.
In dev/,
make html will generate in dev/html/ "clickable version of mlis". (as
the caml standard library)
make coq.pdf will generate nearly the same awfull stuff that coq.ps was.
make {kernel,lib,parsing,..}.{dot,png} will do the dependancy graph of
the given directory.
ocamldoc comment syntax is here :
http://caml.inria.fr/pub/docs/manual-ocaml/manual029.html
The possibility to put graphs in pdf/html seems to be lost.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12969 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
so that we can return the right error message when trying to
declare a scheme twice.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12965 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This is a fairly large commit (around 140 files and 7000 lines of code
impacted), it will cause some troubles for sure (I've listed the know
regressions below, there is bound to be more).
At this state of developpement it brings few features to the user, as
the old tactics were
ported with no change. Changes are on the side of the developer mostly.
Here comes a list of the major changes. I will stay brief, but the code
is hopefully well documented so that it is reasonably easy to infer the
details from it.
Feature developer-side:
* Primitives for a "real" refine tactic (generating a goal for each
evar).
* Abstract type of tactics, goals and proofs
* Tactics can act on several goals (formally all the focused goals). An
interesting consequence of this is that the tactical (. ; [ . | ... ])
can be separated in two
tacticals (. ; .) and ( [ . | ... ] ) (although there is a conflict for
this particular syntax). We can also imagine a tactic to reorder the
goals.
* Possibility for a tactic to pass a value to following tactics (a
typical example is
an intro function which tells the following tactics which name it
introduced).
* backtracking primitives for tactics (it is now possible to implement a
tactical '+'
with (a+b);c equivalent to (a;c+b;c) (itself equivalent to
(a;c||b;c)). This is a valuable
tool to implement tactics like "auto" without nowing of the
implementation of tactics.
* A notion of proof modes, which allows to dynamically change the parser
for tactics. It is controlled at user level with the keywords Set
Default Proof Mode (this is the proof mode which is loaded at the start
of each proof) and Proof Mode (switches the proof mode of the current
proof) to control them.
* A new primitive Evd.fold_undefined which operates like an Evd.fold,
except it only goes through the evars whose body is Evar_empty. This is
a common operation throughout the code,
some of the fold-and-test-if-empty occurences have been replaced by
fold_undefined. For now,
it is only implemented as a fold-and-test, but we expect to have some
optimisations coming some day, as there can be a lot of evars in an
evar_map with this new implementation (I've observed a couple of
thousands), whereas there are rarely more than a dozen undefined ones.
Folding being a linear operation, this might result in a significant
speed-up.
* The declarative mode has been moved into the plugins. This is made
possible by the proof mode feature. I tried to document it so that it
can serve as a tutorial for a tactic mode plugin.
Features user-side:
* Unfocus does not go back to the root of the proof if several Focus-s
have been performed.
It only goes back to the point where it was last focused.
* experimental (non-documented) support of keywords
BeginSubproof/EndSubproof:
BeginSubproof focuses on first goal, one can unfocus only with
EndSubproof, and only
if the proof is completed for that goal.
* experimental (non-documented) support for bullets ('+', '-' and '*')
they act as hierarchical BeginSubproof/EndSubproof:
First time one uses '+' (for instance) it focuses on first goal, when
the subproof is
completed, one can use '+' again which unfocuses and focuses on next
first goal.
Meanwhile, one cas use '*' (for instance) to focus more deeply.
Known regressions:
* The xml plugin had some functions related to proof trees. As the
structure of proof changed significantly, they do not work anymore.
* I do not know how to implement info or show script in this new engine.
Actually I don't even know what they were suppose to actually mean in
earlier versions either. I wager they would require some calm thinking
before going back to work.
* Declarative mode not entirely working (in particular proofs by
induction need to be restored).
* A bug in the inversion tactic (observed in some contributions)
* A bug in Program (observed in some contributions)
* Minor change in the 'old' type of tactics causing some contributions
to fail.
* Compilation time takes about 10-15% longer for unknown reasons (I
suspect it might be linked to the fact that I don't perform any
reduction at QED-s, and also to some linear operations on evar_map-s
(see Evd.fold_undefined above)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12961 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Reasoning modulo variable aliases induced an extra lookup in the
environment at each inversion of the components of the evar instances:
precomputing the aliases map allowed to gain a factor n.
Moreover, solve_evar_evar_l2r was recomputing the evar substitution
from the evar instance n more times than needed.
Function solve_evar_evar_l2r is still on O(n^2) but it does not seem
to be used so often actually. The trivial case has been optimized
(linear time) but the general case could probably be also cut down to
O(n*log(n)) if needed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12939 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The csdp path computed by the configure script wasn't used at all, but
was forcing presence of csdp at configure time whereas it is not used
at all in the build process. Instead, we replace the configure-time
check with a runtime check for existence of csdp in $PATH.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12929 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12879 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
some contribs by >30%) (BACKPORT 12768)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12769 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
dependency order of obligations that was not backwards-compatible.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
* Unicodetable: Update with the standard table for lower case conversion.
* Util: Rewrite "lowercase_unicode" to take the entire unicode character set
into account.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12645 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We renounced to distribute evars to constr and bindings and to let
tactics do the merge. There are now two disciplines:
- the general case is that the holes in tactic arguments are pushed to
the general sigma of the goal so that tactics have no such low-level
tclEVARS, Evd.merge, or check_evars to do:
- what takes tclEVARS and check_evars in charge is now a new
tactical of name tclWITHHOLES (this tactical has a flag to support
tactics in either the "e"- mode and the non "e"- mode);
- the merge of goal evars and holes is now done generically at
interpretation time (in tacinterp) and as a side-effect it also
anticipates the possibility to refer to evars of the goal in the
arguments;
- with this approach, we don't need such constr/open_constr or
bindings/ebindings variants and we can get rid of all ugly
inj_open-style coercions;
- some tactics however needs to have the exact subset of holes known;
this is the case e.g. of "rewrite !c" which morally reevaluates c at
each new rewriting step; this kind of tactics still receive a
specific sigma around their arguments and they have to merge evars
and call tclWITHHOLES by themselves.
Changes so that each specific tactics can take benefit of this generic
support remain to be done.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12603 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
(This should be a conservative extension of the old version.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fixed some bugs in -beautify and robustness of {struct} clause.
Note: I tried to make the Automatic Introduction mode on by default
for version >= 8.3 but it is to complicated to adapt even in the
standard library.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12546 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
[Generalizable (All|No) Variables (ident+)?], also update
type classes documentation to reflect the latest changes
in instance decls. Fix a bug in [Util.list_split_when].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12525 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12520 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
abbreviations of applied references.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12506 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
like the name they refer to).
Fixing buggy test-suite implicit.v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12442 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
against many patterns.
Conflicts:
lib/dnet.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
branch
and remove equations stuff which moves to a separate plugin.
Classes:
- Ability to define classes post-hoc from constants or inductive types.
- Correctly rebuild the hint database associated to local hypotheses when
they are changed by a [Hint Extern] in typeclass resolution.
Tactics and proofs:
- Change [revert] so that it keeps let-ins (but not [generalize]).
- Various improvements to the [generalize_eqs] tactic to make it more robust
and produce the smallest proof terms possible.
Move [specialize_hypothesis] in tactics.ml as it goes hand in hand with
[generalize_eqs].
- A few new general purpose tactics in Program.Tactics like [revert_until]
- Make transitive closure well-foundedness proofs transparent.
- More uniform testing for metas/evars in pretyping/unification.ml
(might introduce a few changes in the contribs).
Program:
- Better sorting of dependencies in obligations.
- Ability to start a Program definition from just a type and no obligations,
automatically adding an obligation for this type.
- In compilation of Program's well-founded definitions, make the functional a
separate definition for easier reasoning.
- Add a hint database for every Program populated by [Hint Unfold]s for
every defined obligation constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12440 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12417 85f007b7-540e-0410-9357-904b9bb8a0f7
|
