| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16292 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16165 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15413 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
|
| |
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
| |
Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.
+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15020 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14725 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This way, no more error messages like "Unrecognized predicate".
Some code simplification and reorganization on the way, in particular
a few tests like "is_Prop ..." or "closed0 ..." were actually useless.
Also add support for the situation H:~Zne x y for uniformity.
Beware: scripts relying negatively on the strength of omega may have to
be adapted (e.g. "try omega. some_more_tactics_in_case_omega_fails.").
For instance, one line deletion in PermutSetoid.v
Probably more cumbersome : "auto with *" becomes stronger since it
may call omega. Todo : check the impact on contribs tomorrow.
Btw, this commit seems to solve a bug where omega was to be guided
by some (set foo:= ...) before being able to succeed (cf PermutSetoid.v)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14474 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14472 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
Util: Added list_assoc_f
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14350 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14348 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
For instance inj_plus is now Nat2Z.inj_add
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14108 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
For instance, former Pplus_plus is now Pos2Nat.inj_add.
As usual, compatibility notation are provided.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14099 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13744 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13637 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
| |
Functions from Termops were sometimes fully qualified, sometimes not
in the same module. This commit makes their usage more uniform.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13470 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- A richer OrderedTypeFull interface : OrderedType + predicate "le"
- Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
- By the way: as suggested by S. Lescuyer, specification of compare is
now inductive
- GenericMinMax: axiomatisation + properties of min and max out of
OrderedTypeFull structures.
- MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
with also some domain-specific results, and compatibility layer
with already existing results.
- Some ML code of plugins had to be adapted, otherwise wrong "eq",
"lt" or simimlar constants were found by functions like coq_constant.
- Beware of the aliasing problems: for instance eq:=@eq t instead of
eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
instead of Z in statement of Zmax_spec).
- Some Morphism declaration are now ambiguous: switch to new syntax
anyway.
- Misc adaptations of FSets/MSets
- Classes/RelationPairs.v: from two relations over A and B, we
inspect relations over A*B and their properties in terms of classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(uniformisation of function names, classification). One of the most
visible change is the renaming of section_path into full_path (the
use of name section was obsolete due to the module system, but I
don't know if the new name is the best chosen one - especially it
remains some "sp" here and there).
- Simplification of the interface of classify_object (first argument dropped).
- Simplification of the code for vernac keyword "End".
- Other small cleaning or dead code removal.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12265 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- add coqtop option "-compat X.Y" so as to provide compatibility with
previous versions of Coq (of course, this requires to take care of
providing flags for controlling changes of behaviors!),
- add support for option names made of an arbitrary length of words
(instead of one, two or three words only),
- add options for recovering 8.2 behavior for discriminate, tauto,
evar unification ("Set Tactic Evars Pattern Unification", "Set
Discriminate Introduction", "Set Intuition Iff Unfolding").
Update of .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12258 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
user contribs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7
|
letouzey
ppedrot
regisgia
herbelin
pboutill
puech
glondu