| Age | Commit message (Collapse) | Author |
|---|
|
No need to tell the world about the fact that constraints are
implemented via caml's Set. Other modules just need to know about
the empty and union functions (and addition functions "enforce_geq"
and "enforce_eq" that were already there).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The gains on contribs are quite small, around 3% max, apart from
3 small contribs where it's about 10% (corresponding to 10s each).
With last patch, we add quicker lookup for universes in the graph
(up to 5 times less calls to cmp_univ_level on an example), but
probably more "administrative" work (i.e. addition of updated paths
in the graphs, handling pairs of updated graphs and results in
functions, etc), and some sharing might also have been lost since
graphs changed more.
Anyway, little gain and more complex code, let's remove this patch
for now ... until the next attempt to speed-up the universe layer.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13724 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
We'll see experimentally if this helps... A few more functions could
be adapted (e.g. between), and an occurence of compare just discard
the compacted graph (in compare_greater)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13723 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
By writing y instead of 0 in the branch where y is 0,
Coq can see that (modulo x y) is a structural subterm of y
(but not necessarily a strict one).
Same trick for div, but here it doesn't help.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13722 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13721 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The auxiliary variable q is now increased continuously instead
of being doubled from time to time. Interest: this version is
obviously linear, and specification proofs are slightly simplier.
NB: the previous version was in fact also linear I think, but
proving this requires a proper complexity analysis.
I'm sure this algorithm is related with some cellular automata
stuff in the spirit of the firing squad :-)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13720 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- The "compare" function on universes (the one answering EQ|LT|LE|NLE)
was launching "collect" for creating the transitive upward closure
of u, and then checking if v is in it. We now proceed more lazily,
by stopping creating the transitive closure as soon as v is found.
- In univ_entry, the first arg u of Equiv(u,v) is removed. It can
indeed be retrieved from the key of the universe graph leading
to this Equiv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13719 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Apparently, it seems that clenv.evd is either created
from dummy_goal (in (e)auto) or from a copy of gls (in
class_tactics). I've checked experimentally by some assert
that on the stdlib the defined part of clenv.evd is always
included in gls. I hence propose to simplify this function
connect_clenv.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Some functions are restricted to consider only undefined evars,
and some Evd.fold are replaced by Evd.fold_undefined. I'm less
sure about the modifications in rewrite.ml4, but in pratice
they seem to work well on the stdlib. I was planning to
say assert false for Not_found in Rewrite.evd_of_existentials
but some file of the stdlib doesn't like that (to be checked).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13717 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- A Evd.defined_evars to keep only this part of the evar_map
- One Evd.fold less in Typeclasses.mark_unresolvables
- We check that only undefined evar_map could be set unresolvable
- A duplicated function in himsg.ml
TODO: some calls to Evd.fold(_undefined) would be faster if written
as Map.map or Map.mapi.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13716 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
indentation depth.
Patch by Cedric Auger.
These two indenters need to be exercised a bit to see if they are actually useful to users.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Patch by Cedric Auger.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13714 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
+-----------------------------------+
| Find: ************** [Find again] |
| Replace With: ****** [Repl.&Find] |
| [?] Search backward [ Close ] |
+-----------------------------------+
Ctrl+b (un)checks "Search backward",
Return searches again,
Ctrl+r replaces and searches again,
Esc close the dialog box.
Patch by Cedric Auger.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13713 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Needed for FreeBSD. Patch by Cedric Auger.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13712 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13711 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13710 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13709 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Patch by David Baelde.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13707 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13704 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
placed by vm_cast_no_check
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13703 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
To avoid names¬ations clashs with list, Vector shouldn't be
"Import"ed but one can "Import Vector.VectorNotations." to have
notations.
SetoidVector at least remains to do.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13702 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13698 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13696 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Now we have:
- Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder
of a/2 is 0 or 1, operations related with two's-complement Zshiftr.
- Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a,
remainder of a/2 is 0 or Zsgn a.
Ok, I'm introducing an incompatibility here, but I think coherence is
really desirable. Anyway, people using Zdiv on positive numbers only
shouldn't even notice the change. Otherwise, it's just a matter of
sed -e "s/div2/quot2/g".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13695 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13694 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
symbol).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13691 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
See NatInt/NZBits.v for the common axiomatization of bitwise functions
over naturals / integers. Some specs aren't pretty, but easier to
prove, see alternate statements in property functors {N,Z}Bits.
Negative numbers are considered via the two's complement convention.
We provide implementations for N (in Ndigits.v), for nat (quite dummy,
just for completeness), for Z (new file Zdigits_def), for BigN
(for the moment partly by converting to N, to be improved soon)
and for BigZ.
NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
the reversed order (for consistency with the rest of the world):
for instance BigN.shiftl 1 10 is 2^10.
NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
on negative numbers. For the moment I've kept it intact, and have
just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
To reorganize someday ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13689 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
With camlp5 6.02.1, this fixes "Print Grammar" in coqide.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13687 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This fixes bug #2442.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13683 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It is in section "My goal is ..., how can I prove it?" of the FAQ.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13681 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Thanks to Marc Lasson for the analysis of the problem and for the
initial patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
this fixes #2441 (even though some other problem was involved too that
r16673 might have solved).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13677 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
in coqdoc index files).
Bug #2183 was fixed by changing "module" into "moduleid" in Index.type_name
instead of changing "moduleid" into "module". But "moduleid" is used
for building the html indexes what led to not very nice output (one
would expect to see "module" in the index).
Apparently, the reason "moduleid" was used instead of "module" as
internal name for rendering module in the TeX output of coqdoc was
that there were already an old \coqdocmodule historically introduced
by Jean-Christophe to format libraries. But this \coqdocmodule seems
to have been replaced by a \coqlibrary by Matthieu in r11065. So I
conclude that Jean-Christophe's use of \coqdocmodule in coqdoc.sty is
definitively obsolete, that the \coqmodule LaTeX command is free for
other uses and that \coqdocmoduleid has no reason not to be called
\coqdocmodule, and consequently, module has no reason to be some
moduleid in Index.type_name.
Moreover, it remained a \moduleid in Output.module_ref ? Shouldn't it
be \coqdocmoduleid (or actually \coqdocmodule, since the id suffix is
apparently no longer needed).
Hoping I'm not doing something wrong.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13675 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- single quotes in notations were breaking coqdoc, even raising an
out-of-bound error when appearing in the last character of the notation;
- letter "x" in notation tokens were inelegantly surrounded by single quotes,
- rare, but allowed characters < 32 were lost in index pages.
A new fully injective space-free-and-human-readable encoding algorithm
is adopted which put single quotes around all terminal tokens,
double existing single quotes, and replace invisible characters by
^X-like strings.
Moreover, the keywords "Local"/"Global" were blocking the detection of
keywords starting coq lines (e.g. "Local Notation" was not recognized
as a notation). "Local" and "Global" are now uniformly treated as
modifiers of vernac commands as they are in the Coq parser.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13673 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This fixes "Print Grammar" in coqide, which uses a camlp5 function
that prints to stdout, interfering with the ide-slave
communication. Camlp5 should additionnally provide a way to print to a
formatter instead of directly using stdout...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13670 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13669 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@13666 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13665 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13664 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13663 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Fix a bug in [comp_term] (casts were ignored).
- Improve the efficiency of hash table lookup.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13662 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Remove an unsound optimization.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13661 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Fix an efficiency bug when hash-consing deep [constr]s.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13660 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Non-dependent products in formulas were turned into implications,
leading to some issues.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13656 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13655 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Well, hopefully, that belongs to the past: you should now be able
to do the very same queries as before, without typing the [ ].
For instance: SearchAbout plus mult.
This removal of [ ] is optional, the old syntax is still legal:
- for compatibility reasons
- for square bracket lovers
- for those that have "inside" or "outside" as legal identifier
in their development and want to search about them.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13654 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13653 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13652 85f007b7-540e-0410-9357-904b9bb8a0f7
|
