| Age | Commit message (Collapse) | Author |
|---|
|
... no need to Unset them manually
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
When arguments scopes are set manually, nothing new, they stay
as they are (until maybe another Arguments invocation).
But when argument scopes are computed out of the argument type and
the Bind Scope information, this kind of scope is now dynamic:
a later Bind Scope will be able to impact the scopes of an earlier
constant. For Instance:
Definition f (n:nat) := n.
About f. (* Argument scope is [nat_scope] *)
Bind Scope other_scope with nat.
About f. (* Argument scope is [other_scope] *)
This allows to get rid of hacks for modifying scopes during functor
applications. Moreover, the subst_arguments_scope is now
environment-insensitive (needed for forthcoming changes in declaremods).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16350 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The offending functor in NZOrder wasn't actually used, so
I've commented it for now.
Btw, the Not_found in coqchk is now turned into something slightly
more informative
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16199 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
It is much beter for everything (includind guard condition and simpl refolding)
excepts typeclasse inference because unification does not recognize
(fun x => f x b) a when it sees f a b ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16112 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Inner sub-modules with "Definition t := t" is hard to handle by
extraction: "type t = t" is recursive by default in OCaml, and
the aliased t cannot easily be fully qualified if it comes from
a higher unterminated module. There already exists some workarounds
(generating Coq__XXX modules), but this isn't playing nicely with
module types, where it's hard to insert code without breaking
subtyping.
To avoid falling too often in this situation, I've reorganized:
- GenericMinMax : we do not try anymore to deduce facts about
min by saying "min is a max on the reversed order". This hack
was anyway not so nice, some code was duplicated nonetheless
(at least statements), and the module structure was complex.
- OrdersTac : by splitting the functor argument in two
(EqLtLe <+ IsTotalOrder instead of TotalOrder), we avoid
the need for aliasing the type t, cf NZOrder.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16052 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15930 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15838 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:
destruct x eqn:H
destruct x as [ ] eqn:H
Some with induction. Of course, the pattern behind "as" is arbitrary.
For an anonymous version, H could be replaced by ?. The old syntax
with "_eqn" still works for the moment, by triggers a warning.
For making this new syntax work, we had to change the seldom-used
"induction x y z using foo" into "induction x, y, z using foo".
Now, only one "using" can be used per command instead of one per
comma-separated group earlier, but I doubt this will bother anyone.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- For instance, refl_equal --> eq_refl
- Npos, Zpos, Zneg now admit more uniform qualified aliases
N.pos, Z.pos, Z.neg.
- A new module BinInt.Pos2Z with results about injections from
positive to Z
- A result about Z.pow pushed in the generic layer
- Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
- Using tactic Z.le_elim instead of Zle_lt_or_eq
- Some cleanup in ring, field, micromega
(use of "Equivalence", "Proper" ...)
- Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
- In ZMake and ZMake, functor parameters are now named NN and ZZ
instead of N and Z for avoiding confusions
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14718 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
This adds two experimental features to the typeclass implementation:
- Path cuts: a way to specify through regular expressions on instance names
search pathes that should be avoided (e.g. [proper_flip proper_flip]).
Regular expression matching is implemented through naïve derivatives.
- Forward hints for subclasses: e.g. [Equivalence -> Reflexive] is no
longer applied backwards, but introducing a specific [Equivalence] in the
environment register a [Reflexive] hint as well. Currently not
backwards-compatible, the next patch will allow to specify direction
of subclasses hints.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14671 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14413 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Instead of hard-coding in search.ml some substrings such
as "_admitted" or "_subproof" we don't want to see in results
of SearchAbout and co, we now have a user command:
Add Search Blacklist "foo".
Remove Search Blacklist "foo". (* the opposite *)
Print Table Search Blacklist. (* the current state *)
In Prelude.v, three substrings are blacklisted originally:
- "_admitted" for internal lemmas due to admit.
- "_subproof" for internal lemmas due to abstract.
- "Private_" for hiding auxiliary modules not meant for
global usage.
Note that substrings are searched in the fully qualified names
of the available lemmas (e.g. "Coq.Init.Peano.plus").
This commit also adds the prefix "Private_" to some internal modules
in Numbers, Z, N, etc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14408 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z
- The alternative Zpower_alt is now in a separate file Zpow_alt.v,
not loaded by default.
- Some more injection lemmas in Znat (pow, div, mod, quot, rem)
- Btw, added a "square" function in Z, N, Pos, ... (instead of
Zpow_facts.Zsquare).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Note that in NSig (and hence NMake and BigN), to_N is now
Z.to_N (to_Z ...) instead of Z.abs_N (to_Z ...). This doesn't
change the result (since to_Z create non-negative integers),
but some proofs may have to be adapted
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14250 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- No need for compatibility notations for stuff introduced strictly
after branching of 8.3, for instance Nor, Nand, etc.
- Properties for N.lor, N.lxor, etc are now in BinNat.N, no need to
duplicate them in Ndigits, apart from the few compatibility results
about xor.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14249 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14246 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14245 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14244 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In particular, we merge the old Zdivide (used to be an ad-hoc
inductive predicate) and the new Z.divide (based on exists).
Notations allow to do that (almost) transparently, the only
impact is that the name picked by the system will not be "q"
anymore when destructing a Z.divide. Some fragile scripts
may have to be fixed.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14239 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14238 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14237 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14234 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14230 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14229 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Start of a uniform treatment of compare, eqb, leb, ltb:
- We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos
- Some generic properties are derived in OrdersFacts.BoolOrderFacts
In BinPos, more work about sub_mask with nice implications
on compare (e.g. simplier proof of lt_trans).
In BinNat/BinPos, for uniformity, compare_antisym is now
(y ?= x) = CompOpp (x ?=y) instead of the symmetrical result.
In BigN / BigZ, eq_bool is now eqb
In BinIntDef, gtb and geb are kept for the moment, but
a comment advise to rather use ltb and leb. Z.div now uses
Z.ltb and Z.leb.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14226 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
All the functions about Z is now in a separated file BinIntDef,
which is Included in BinInt.Z. This BinInt.Z directly
implements ZAxiomsSig, and instantiates derived properties ZProp.
Note that we refer to Z instead of t inside BinInt.Z,
otherwise ring breaks later on @eq Z.t
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
A sub-module N in BinNat now contains functions add (ex-Nplus),
mul (ex-Nmult), ... and properties.
In particular, this sub-module N directly instantiates NAxiomsSig
and includes all derived properties NProp.
Files Ndiv_def and co are now obsolete and kept only for compat
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14100 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
BinPos now contain a sub-module Pos, in which are placed functions
like add (ex-Pplus), mul (ex-Pmult), ... and properties like
add_comm, add_assoc, ...
In addition to the name changes, the organisation is changed quite
a lot, to try to take advantage more of the orders < and <= instead
of speaking only of the comparison function.
The main source of incompatibilities in scripts concerns this compare:
Pos.compare is now a binary operation, expressed in terms of the
ex-Pcompare which is ternary (expecting an initial comparision as 3rd arg),
this ternary version being called now Pos.compare_cont. As for everything
else, compatibility notations (only parsing) are provided. But notations
"_ ?= _" on positive will have to be edited, since they now point to
Pos.compare.
We also make the sub-module Pos to be directly an OrderedType,
and include results about min and max.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14098 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
In the coming reorganisation, the name Z in BinInt will be a
module containing all code and properties about binary integers.
The inductive type Z hence cannot be at the same location.
Same for N and positive. Apart for this naming constraint, it
also have advantages : presenting the three types at once is
clearer, and we will be able to refer to N in BinPos (for instance
for output type of a predecessor function on positive).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
checking types.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14023 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13943 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
CompareSpec expects 3 propositions Peq Plt Pgt instead of 2 relations
eq lt and 2 points x y. For the moment, we still always use (Peq=eq x y),
(Plt=lt x y) (Pgt=lt y x), but this may not be always the case,
especially for Pgt. The former CompSpec is now defined in term of
CompareSpec. Compatibility is preserved (except maybe a rare unfold
or red to break the CompSpec definition).
Typically, CompareSpec looks nicer when we have infix notations, e.g.
forall x y, CompareSpec (x=y) (x<y) (y<x) (x?=x)
while CompSpec is shorter when we directly refer to predicates:
forall x y, CompSpec eq lt x y (compare x y)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13914 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion when checking types of instanciations while having
restricted delta reduction for unification itself. This
makes auto/eauto... backward compatible.
- Change semantics of [Instance foo : C a.] to _not_ search
for an instance of [C a] automatically and potentially slow
down interaction, except for trivial classes with no fields.
Use [C a := _.] or [C a := {}] to search for an instance of
the class or for every field.
- Correct treatment of transparency information for classes
declared in sections.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
Initial patch by Robbert Krebbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13900 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13851 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
conversion.
- Fix trans_fconv* to use evars correctly.
- Normalize the goal with respect to evars before rewriting in
[rewrite], allowing to see instanciations from other subgoals.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13844 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
For Argument Scope, we now record types (more precisely classes cl_typ)
in addition to scope list. After substitution (e.g. at functor application),
the new types are used to search for corresponding concrete scopes.
Currently, this automatic scope substitution of argument scope takes
precedence (if successful) over scope declared in the functor (even
by the user). On the opposite, the manual scope substitution
(cf last commit introducing annotation [scope foo to bar])
is done _after_ the automatic scope substitution.
TODO: if this behavior is satisfactory, document it ...
Note that Classops.find_class_type lose its env args since it was
actually unused, and is now used for Notation.find_class
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13840 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
- The experimental syntax "<30>F M" is transformed into "F M [inline at level 30]"
- The earlier syntax !F X should now be written "F X [no inline]"
(note that using ! is still possible for compatibility)
- A new annotation "F M [scope foo_scope to bar_scope]" allow to substitute
foo_scope by bar_scope in all arguments scope of objects in F.
BigN and BigZ are cleaned from the zillions of Arguments Scope used earlier.
Arguments scope for lemmas are fixed for instances of Numbers.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13839 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
|
|
We now specify testbit by some initial and recursive equations.
The previous spec (via a complex split of the number in
low and high parts) is now a derived property in {N,Z}Bits.v
This way, proofs of implementations are quite simplier.
Note that these new specs doesn't imply anymore that testbit is a
morphism, we have to add this as a extra spec (but this lead
to trivial proofs when implementing).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13792 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
|
