| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
|
|
| |
evar, and simultaneously make type inference with universes work better.
This only exports more functions from kernel/univ, to be able to work
with a set of universe variables during type inference. Universe
constraints are gradually added during type checking, adding information
necessary e.g. to lower the level of unknown Type variables to Prop or
Set. There does not seem to be a disastrous performance hit on the
stdlib, but might have one on some contribs (hence the "Tentative").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13905 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13897 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13891 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13890 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
This happens for instance when the main component of the fixpoint
block has been provided via Extract Constant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13889 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a mix of "Recursive Extraction" and "Extraction Library":
- like "Extraction Library", the extracted code is splitted in
separated files, one per coq source file.
- unlike "Extraction Library", but similarly to "Recursive Extraction",
not everything gets extracted, but only dependencies of some
initially-given elements
We prepare for a more clever dependency selection inside sub-modules.
For the moment all needed sub-modules are still fully extracted (other we
would need to fix signatures accordingly).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13888 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
for the domain instead of retrieving the known domain of the initial evar.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13881 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For Haskell, we still try to provide readable indentation,
but we now avoid relying on this indentation for correctness.
Instead, we use layout-independant syntax with { } when
necessary (after "case of" and "let"). It is much safer this
way, even if the syntax gets a bit more cumbersome.
For people allergic to {;}, they can most of the time do a
tr -d "{;}" without changing the meaning of the program.
Be careful nonetheless: since "case of" is now delimited,
some parenthesis that used to be mandatory are now removed.
Note also that the initial "module ... where" is still without
{ }: even when Format goes crazy it doesn't tamper with column 0.
Other modifications:
- Using "Set Printing Width" now affects uniformly the extraction
pretty-printers. You can set a greater value than the default 78
before extracting a program that you know to be "really deep".
- In ocaml (and also a bit in Haskell), we now try to avoid abusing
of 2-char-right-indentation. For instance | is now aligned with
the "m" of match. This way, max_indent will be reached less frequently.
- As soon as a pretty-print box contains an explicit newline,
we set its virtual size to a big number, in order to prevent this
box to be part of some horizontal arrangement.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13870 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
application of a dummy "obligation" constant.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13863 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13861 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13859 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
This reverts pottier's commit r13849. It references a
ncring_plugin.cma for which there is no rule. I guess he forgot to
commit something...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13856 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13849 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13848 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
intern_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Everything seems to work fine in CoqIDE (except escape/return and the daimon which are not entirely ported).
However, there is some problem causing proof general to fail when using goto or evaluate buffer (evaluate next phrase works fine though), as well as coqc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13817 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13811 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
As said in CHANGES:
<<
The inlining done during application of functors can now be controlled
more precisely. In addition to the "!F G" syntax preventing any inlining,
we can now use a priority level to select parameters to inline :
"<30>F G" means "only inline in F the parameters whose levels are <= 30".
The level of a parameter can be fixed by "Parameter Inline(30) foo".
When levels aren't given, the default value is 100. One can also use
the flag "Set Inline Level ..." to set a level.
>>
Nota : the syntax "Parameter Inline(30) foo" is equivalent to
"Set Inline Level 30. Parameter Inline foo.",
and "Include <30>F G" is equivalent to "Set Inline Level 30. Include F G."
For instance, in ZBinary, eq is @Logic.eq and should rather be inlined,
while in BigZ, eq is (fun x y => [x]=[y]) and should rather not be inlined.
We could achieve this behavior by setting a level such as 30 to the
parameter eq, and then tweaking the current level when applying functors.
This idea of levels might be too restrictive, we'll see, but at least
the implementation of this change was quite simple. There might be
situation where parameters cannot be linearly ordered according to their
"inlinablility". For these cases, we would need to mention names to inline
or not at a functor application, and this is a bit more tricky
(and might be a pain to use if there are many names).
No documentation for the moment, since this feature is experimental
and might still evolve.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13807 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13770 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
| |
Rationale: the expansion ignores the TYPED clause when
{RAW,GLOB}_TYPED are given. Indeed, in this case, the final type is a
consequence of either "INTERPRETED BY" (if given), or the default one
based on GLOB_TYPED.
This avoids the pitfall of the "raw" argument extension, where the
TYPED clause was unused and totally misleading.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13760 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
perl -pi -e 's/(mk)R(Ref|Var|Evar|PatVar|App|Lambda|Prod|LetIn|Case
s|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic|Prop|Type|Fix|CoFix|Struct
Rec|WfRec|MeasureRec)/\1G\2/g' **/*.ml*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13758 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13757 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
| |
perl -pi -e 's/(\W|_)raw((?:sort|_prop|terms?|_branch|_red_flag|pat
tern|_constr_of|_of_pat)(?:\W|_))/\1glob_\2/g;s/glob__/glob_/g;s/(\
W)R((?:Prop|Type|Fix|CoFix|StructRec|WfRec|MeasureRec)\W)/\1G\2/g;s
/glob_terms?/glob_constr/g' **/*.ml*
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13756 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13755 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
There was a discrepancy of the notions "raw" and "globalized" between
constrs and tactics, and some confusion of the notions in
e.g. genarg.mli (see all globwit_* there). This commit is a first step
towards unification of terminology between constrs and
tactics. Changes in module names will be done separately.
In extraargs.ml4, the "ARGUMENT EXTEND raw" and related stuff, even
affected by this change, has not been touched and highlights another
confusion in "ARGUMENT EXTEND" in general that will be addressed
later.
The funind plugin doesn't respect the same naming conventions as the
rest, so leave some "raw" there for now... they will be addressed
later.
This big commit has been generated with the following command (wrapped
here, but should be on a *single* line):
perl -pi -e 's/(\W(?:|pp|pr_l)|_)raw((?:constrs?|type|vars|_binder|
_context|decl|_decompose|_compose|_make)(?:\W|_))/\1glob_\2/g;s/glo
b__/glob_/g;s/prraw/prglob/g;s/(\W)R((?:Ref|Var|Evar|PatVar|App|Lam
bda|Prod|LetIn|Cases|LetTuple|If|Rec|Sort|Hole|Cast|Dynamic)\W)/\1G
\2/g' `git ls-files|grep -v dev/doc/changes.txt`
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13743 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13742 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
| |
We now keep some type information in the "info" field of constructors
and cases, and compact a match with some default branches (or remove
this match completely) only if this transformation is type-preserving.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13732 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13711 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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.
Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)
PArith/BinPos:
- added a power function Ppow
- iterator iter_pos moved from Zmisc to here + some lemmas
- added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
- more lemmas on Pcompare and succ/+/* and order, allow
to simplify a lot some old proofs elsewhere.
- new/revised results on Pminus (including some direct proof of
stuff from Pnat)
PArith/Pnat:
- more direct proofs (limit the need of stuff about Pmult_nat).
- provide nicer names for some lemmas (eg. Pplus_plus instead of
nat_of_P_plus_morphism), compatibility notations provided.
- kill some too-specific lemmas unused in stdlib + contribs
NArith/BinNat:
- N_of_nat, nat_of_N moved from Nnat to here.
- a lemma relating Npred and Nminus
- revised definitions and specification proofs of Npow and Nlog2
NArith/Nnat:
- shorter proofs.
- stuff about Z_of_N is moved to Znat. This way, NArith is
entirely independent from ZArith.
NArith/Ndigits:
- added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
- revised proofs about Nxor, still using functional bit stream
- use the same approach to prove properties of Nand Nor Ndiff
ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff
ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat
ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N
ZArith/Zmisc: almost empty new, only contain stuff about badly-named
iter. Should be reformed more someday.
ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
proofs and avoid slowdown due to adding 1 in Z instead of in positive
Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
as long as I dont't know why it's slower on powers of two.
Elsewhere: propagate new names + some nicer proofs
NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(floor convention).
We follow Haskell naming convention: quot and rem are for
Round-Toward-Zero (a.k.a Trunc, what Ocaml, C, Asm do by default, cf.
the ex-ZOdiv file), while div and mod are for Round-Toward-Bottom
(a.k.a Floor, what Coq does historically in Zdiv). We use unicode รท
for quot, and infix rem for rem (which is actually remainder in
full). This way, both conventions can be used at the same time.
Definitions (and proofs of specifications) for div mod quot rem are
migrated in a new file Zdiv_def. Ex-ZOdiv file is now Zquot. With
this new organisation, no need for functor application in Zdiv and
Zquot.
On the abstract side, ZAxiomsSig now provides div mod quot rem.
Zproperties now contains properties of them. In NZDiv, we stop
splitting specifications in Common vs. Specific parts. Instead,
the NZ specification is be extended later, even if this leads to
a useless mod_bound_pos, subsumed by more precise axioms.
A few results in ZDivTrunc and ZDivFloor are improved (sgn stuff).
A few proofs in Nnat, Znat, Zabs are reworked (no more dependency
to Zmin, Zmax).
A lcm (least common multiple) is derived abstractly from gcd and
division (and hence available for nat N BigN Z BigZ :-).
In these new files NLcm and ZLcm, we also provide some combined
properties of div mod quot rem gcd.
We also provide a new file Zeuclid implementing a third division
convention, where the remainder is always positive. This file
instanciate the abstract one ZDivEucl. Operation names are
ZEuclid.div and ZEuclid.modulo.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13633 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
before the message is delivered to the user. Should avoid useless
computation in heavily backtracking tactics (auto, try, ...).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
types" occurs. Also improved the "unexpected type" error message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
Beware! after this, a ./configure must be done. It might also
be a good idea to chase any phantom .vo remaining after a make clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13601 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
option of "auto". Works for not too complicated hints (e.g. "@pair _ _ 0").
Would be simpler if make_apply_entry supported lemmas containing evars.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13598 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13597 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
- NPeano isn't Exported by default anymore (contains pow for nat).
- in coq_micromega.ml, we specify more where to find the pow of R.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13569 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13568 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13554 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13542 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
|
| |
no undefined variables in the context now).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13532 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
|
|
| |
in addition, a makefile entry pluginsopt for compiling only the .cmxs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13509 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13505 85f007b7-540e-0410-9357-904b9bb8a0f7
|