aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
Commit message (Collapse)AuthorAge
* Use generalizable variables info when internalizing arbitrary bindings,Gravatar msozeau2009-11-08
| | | | | | | not just type class applications. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12479 85f007b7-540e-0410-9357-904b9bb8a0f7
* Numbers: finish files NStrongRec and NDefOpsGravatar letouzey2009-11-06
| | | | | | | | | | | | | | | | | | - NStrongRec provides a "strong" recursor based on the usual one: recursive calls can be done here on any lower value. See binary log in NDefOps for an example of use. - NDefOps contains alternative definitions of usual operators (add, mul, ltb, pow, even, half, log) via usual or strong recursor, and proofs of correctness and/or of equivalence with axiomatized operators. These files were in the archive but not being compiled, some proofs of correction for functions defined there were missing. By the way, some more iff-style lemmas in Bool. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
| | | | | | | | | | | | | | | | | | | | | | | | - 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
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12458 85f007b7-540e-0410-9357-904b9bb8a0f7
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
| | | | | | | | | | | | | | | | | This allows easier handling of dependencies, for instance RelationClasses won't have to requires List (which itself requires part of Arith, etc). One of the underlying ideas is to provide setoid rewriting in Init someday. Thanks to some notations in List, this change should be fairly transparent to the user. For instance, one could see that List.length is a notation for (Datatypes.)length only when doing a Print List.length. For these notations not to be too intrusive, they are hidden behind an explicit Export of Datatypes at the end of List. This isn't very pretty, but quite handy. Notation.ml is patched to stop complaining in the case of reloading the same Delimit Scope twice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12452 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
| | | | | | | | | | | | | variables with syntax: [Local?|Global] Generalizable Variable(s)? [all|none|id1 idn]. By default no variable is generalizable, so this patch breaks backward compatibility with files that used implicit generalization (through Instance declarations for example). To get back the old behavior, one just needs to use [Global Generalizable Variables all]. Make coq_makefile more robust using [mkdir -p]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12428 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix new instances that could easily make class resolution loop on Gravatar msozeau2009-10-22
| | | | | | | | unconstrained goals (e.g. PreOrder A ?). Allow the unconstrained use of [proper_reflexive] again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12407 85f007b7-540e-0410-9357-904b9bb8a0f7
* MSets: a new generation of FSetsGravatar letouzey2009-10-13
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Same global ideas (in particular the use of modules/functors), but: - frequent use of Type Classes inside interfaces/implementation. For instance, no more eq_refl/eq_sym/eq_trans, but Equivalence. A class StrictOrder for lt in OrderedType. Extensive use of Proper and rewrite. - now that rewrite is mature, we write specifications of set operators via iff instead of many separate requirements based on ->. For instance add_spec : In y (add x s) <-> E.eq y x \/ In x s. Old-style specs are available in the functor Facts. - compare is now a pure function (t -> t -> comparison) instead of returning a dependent type Compare. - The "Raw" functors (the ones dealing with e.g. list with no sortedness proofs yet, but morally sorted when operating on them) are given proper interfaces and a generic functor allows to obtain a regular set implementation out of a "raw" one. The last two points allow to manipulate set objects that are completely free of proof-parts if one wants to. Later proofs will rely on type-classes instance search mechanism. No need to emphasis the fact that this new version is severely incompatible with the earlier one. I've no precise ideas yet on how allowing an easy transition (functors ?). For the moment, these new Sets are placed alongside the old ones, in directory MSets (M for Modular, to constrast with forthcoming CSets, see below). A few files exist currently in version foo.v and foo2.v, I'll try to merge them without breaking things. Old FSets will probably move to a contrib later. Still to be done: - adapt FMap in the same way - integrate misc stuff like multisets or the map function - CSets, i.e. Sets based on Type Classes : Integration of code contributed by S. Lescuyer is on the way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
| | | | | | | | | This allow in particular to write eq instead of (@eq _) in signatures of morphisms. I dont really see how this could break existing code, no change in the stdlib was mandatory. We'll check the contribs tomorrow... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
| | | | | | | | | | existentials are generated (at last!). The code simply keeps failure continuations and apply them if needed. Fix bottomup and topdown rewrite strategies that looped. Use auto introduction flag for typeclass instances as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12374 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
| | | | | | | | | | | | | | | | | | | 1) compilation of Library.tex was failing on a "Ext_" in Diaconescu.v In fact coqdoc was trying to recognize the end of a _emphasis_ and hence inserted a bogus }. For the moment I've enclosed the phrase with [ ], but this emphasis "feature" of coqdoc seems _really_ easy to broke. Matthieu ? 2) By the way, this Library document was made from latin1 and utf8 source file, hence bogus characters. All .v containing special characters are converted to utf8, and their first line is now mentionning this. (+ killed some old french comments and some other avoidable special characters). PLEASE: let's stick to this convention and avoid latin1, at least in .v files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12363 85f007b7-540e-0410-9357-904b9bb8a0f7
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix compilation errors due to last commit.Gravatar msozeau2009-09-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12333 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using [obligation_tactic] from Program.Tactics as the defaultGravatar msozeau2009-09-15
| | | | | | | | obligation tactic so that [Program] can work without importing anything. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12330 85f007b7-540e-0410-9357-904b9bb8a0f7
* Misc fixes:Gravatar msozeau2009-09-10
| | | | | | | | | | - better implicits for [antisymmetry] - don't throw away implicit arguments info when doing [Program Definition : type.] - add standard debugging tactics to print goals/hyps in Program. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
| | | | | | | | | | | | | | | | | | | rewriting (thanks to Georges Gonthier for pointing it out). We try to find a declared rewrite relation when the equation does not look like an equality and otherwise try to reduce it to find a leibniz equality but don't backtrack on generalized rewriting if this fails. This new behavior make two fsets scripts fail as they are trying to use an underlying leibniz equality for a declared rewrite relation, a [red] fixes it. Do some renaming from "setoid" to "rewrite". Fix [is_applied_rewrite_relation]'s bad handling of evars and the environment. Fix some [dual] hints in RelationClasses.v and assert that any declared [Equivalence] can be considered a [RewriteRelation]. Fix minor tex output problem in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12310 85f007b7-540e-0410-9357-904b9bb8a0f7
* Do a fixpoint on the result of typeclass search to force theGravatar msozeau2009-06-08
| | | | | | | resolution of generated evars, not doing any backtracking yet. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12175 85f007b7-540e-0410-9357-904b9bb8a0f7
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
| | | | | | | as they are used. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
| | | | | | | | | - Set implicit args on for Context decls - Move class_apply tactic to Init - Normalize evars before raising an error. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12127 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements in typeclasses eauto and generalized rewriting:Gravatar msozeau2009-05-05
| | | | | | | | | | | | | - Decorate proof search with depth/subgoal number information - Add a tactic [autoapply foo using hints] to call the resolution tactic with the [transparent_state] associated with a hint db, giving better control over unfolding. - Fix a bug in the Lambda case in the new rewrite - More work on the [Proper] and [subrelation] hints to cut the search space while retaining completeness. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12118 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixes for bugs in r12110:Gravatar msozeau2009-04-28
| | | | | | | | | | - [matches] is not parameterized by evars: normalize before calling conclPattern. - fix hints in Morphisms for subrelation and handling of signature normalization. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12115 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
| | | | | | | | | | | and failure continuations, allowing to do safe cuts correctly. - Fix bug #2097 by suppressing useless nf_evars calls. - Improve the proof search strategy used by rewrite for subrelations and fix some hints. Up to 20% speed improvement in setoid-intensive files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12110 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
| | | | | | | | clause resulting in stray notations for e.g. variable named "le") and 12083 (fixing bug in as clause of apply in) from trunk. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12103 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rename [Morphism] into [Proper] and [respect] into [proper] to complyGravatar msozeau2009-04-21
| | | | | | | with standard math nomenclature. Also clean up in rewrite.ml4. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix wrong pattern in Morphisms. Fix bug scripts to reflect the fact thatGravatar msozeau2009-04-20
| | | | | | | Setoid doesn't export Program.Basics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12095 85f007b7-540e-0410-9357-904b9bb8a0f7
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12094 85f007b7-540e-0410-9357-904b9bb8a0f7
* Only export the notations of Morphism as well as Equivalence throughGravatar msozeau2009-04-17
| | | | | | | Setoid, the rest needs to be qualified. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12093 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better Requires in Classes. Fix bug #2093: the code does not requireGravatar msozeau2009-04-16
| | | | | | | Program.Tactics anymore. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12089 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of setoid_rewrite to modularize it based on proof-producingGravatar msozeau2009-04-13
| | | | | | | | | | | | | | | strategies (à la ELAN). Now setoid_rewrite is just one strategy and autorewrite is a more elaborate one. Any kind of traversals can be defined, strategies can be composed etc... in ML. An incomplete (no fix) language extension for specifying them in Ltac is there too. On a typical autorewrite-with-setoids usage, proof production time is divided by 2 and proof size by 10. Fix some admitted proofs and buggy patterns in Classes.Morphisms as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12081 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move setoid_rewrite to its own module and do some clean up inGravatar msozeau2009-04-07
| | | | | | | class_tactics. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12056 85f007b7-540e-0410-9357-904b9bb8a0f7
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
| | | | | | | | | | | | | | | - The measure can now refer to all the formal arguments - The recursive calls can make all the arguments vary as well - Generalized to any relation and measure (new syntax {measure m on R}) This relies on an automatic curryfication transformation, the real fixpoint combinator is working on a sigma type of the arguments. Reduces to the previous impl in case only one argument is involved. The patch also introduces a new flag on implicit arguments that says if the argument has to be infered (default) or can be turned into a subgoal/obligation. Comes with a test-suite file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12030 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix [subrelation] clauses that privileged the weakest. Better impl argsGravatar msozeau2009-02-04
| | | | | | | for [PartialOrder] typeclass. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11882 85f007b7-540e-0410-9357-904b9bb8a0f7
* Last changes in type class syntax: Gravatar msozeau2009-01-18
| | | | | | | | | | | | - curly braces mandatory for record class instances - no mention of the unique method for definitional class instances Turning a record or definition into a class is mostly a matter of changing the keywords to 'Class' and 'Instance' now. Documentation reflects these changes, and was checked once more along with setoid_rewrite's and Program's. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11797 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
| | | | | | | | | | doc is ok). Rework the .v files in Program accordingly, adding some documentation and proper headers. Integrate the development of an elimination principle for measured functions in Program/Wf by Eelis van der Weegen. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11686 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finish fix for the treatment of [inverse] in [setoid_rewrite], making aGravatar msozeau2008-12-16
| | | | | | | | | | variant of the [unify] tactic that takes a hint db as argument and does unification modulo its [transparent_state]. Add test-file for bug #1939 and another [AdvancedTypeClasses.v] that mimicks [AdvancedCanonicalStructure.v]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11685 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
| | | | | | | | | | | | | | | | | guessing the binding name by default and making all generalized variables implicit. At the same time, continue refactoring of Record/Class/Inductive etc.., getting rid of [VernacRecord] definitively. The AST is not completely satisfying, but leaning towards Record/Class as restrictions of inductive (Arnaud, anyone ?). Now, [Class] declaration bodies are either of the form [meth : type] or [{ meth : type ; ... }], distinguishing singleton "definitional" classes and inductive classes based on records. The constructor syntax is accepted ([meth1 : type1 | meth1 : type2]) but raises an error immediately, as support for defining a class by a general inductive type is not there yet (this is a bugfix!). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix handling of [inverse] in setoid_rewrite, with an hopefully completeGravatar msozeau2008-12-08
| | | | | | | procedure. Brainstormed with Nicolas Tabareau. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11660 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix priority of the Leibniz Setoid instance to 10 (thanks to M. LassonGravatar msozeau2008-12-04
| | | | | | | for the report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11656 85f007b7-540e-0410-9357-904b9bb8a0f7
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
| | | | | | | | | | | | declaration code to toplevel/record, including support for singleton classes as definitions. Parsing code also factorized. Arnaud: one more thing to think about when refactoring the definitions in vernacentries. Add support for specifying what to do with anonymous variables in contexts during internalisation (fixes bug #1982), current choice is to generate a name for typeclass bindings. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11563 85f007b7-540e-0410-9357-904b9bb8a0f7
* Minor fixes:Gravatar msozeau2008-11-05
| | | | | | | | | - Rework definition of the type of respecful functions in Morphisms.v - Unfold [flip] in "Add Morphism" tactic (suggested by N. Tabareau) - Add a "coqvariableref" command in coqdoc. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11545 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
| | | | | | | | | | instead of a completely resolved [constr] as input. The propagation of the evars associated to the lemma is only allowed when the evar flag is on (i.e. for [eapply]), otherwise they should be resolved by the end of the application. Should be completely backwards compatible... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
| | | | | | | | | | | | | | | | | | | | | - New constr_expr construct [CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr] to generalize the free vars of the [constr_expr], binding these using [binding_kind] and making a lambda or a pi (or deciding from the scope) using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) - Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for implicit bindings (both "..(" and "_(" seem much more difficult to implement). Subject to discussion! A few examples added in a test-suite file. - Also add missing syntax for implicit/explicit combinations for _binders_: "{( )}" means implicit for the generalized (outer) vars, explicit for the (inner) variable itself. Subject to discussion as well :) - Factor much typeclass instance declaration code. We now just have to force generalization of the term after the : in instance declarations. One more step to using Instance for records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
| | | | | | | | | | | | [discriminated]] with a switch for using the more experimantal dnet impl for every hint. Also add [Hint Transparent/Opaque] which parameterize the dnet and the unification flags used by auto/eauto with a particular database. Document all this. Remove [Typeclasses unfold] directives that are no longer needed (everything is unfoldable by default) and move to [Typeclasses Transparent/Opaque] syntax. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11409 85f007b7-540e-0410-9357-904b9bb8a0f7
* Use manual implicts in Classes and rationalize class parameter names.Gravatar msozeau2008-09-14
| | | | | | | | | | Now it's [A] and [R] for carriers and relations and [eqA] when the relation is supposed to be an equivalence. The types are always implicit except for [pointwise_relation] which now takes the domain type as an explicit argument. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11408 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remove redefinition of id in Program.Basics, just add maximal implicits.Gravatar msozeau2008-09-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11401 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
| | | | | | | | | recursive definitions and references to previous fields in record and classes definitions. Fixes the corresponding typesetting issue in coqdoc output. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
| | | | | | | | | | | | | | | This permits to create a database [relations] in [RelationClasses] with a single extern tactic in it that tries to apply [reflexivity] or [symmetry]. This is then automatically used in [auto with *] and repair backward compatibility. The previous commit broke some scripts which were using [intuition] to do (setoid) [reflexivity] or [symmetry]: this worked only by accident, because the hint database of typeclasses was used. Overrall, this also allows to put a bunch of always-applicable, related tactics in some database or to use [Hint Extern] but match only on hypotheses. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11384 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improve typeclasses eauto using the dnet for local assumptions too, and selectGravatar msozeau2008-09-04
| | | | | | | | | | only relevant hypotheses in it, slightly cutting the search space. Makes setoid_rewrite less sensitive to the number of hypothesis (~ 5% time improvment on the stdlib). This currently prevents resolution with constants which reduce to classes, hence the modifications in Setoids.Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11360 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1935, reworking the reflexivity, symmetry... tactics to useGravatar msozeau2008-09-03
| | | | | | | | | the same typeclass method application tactic that's available to users. Modify a bit the _red tactics to accomodate the new setup and comment some dead code in setoid_replace. Next step is removing it completely. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major speed and space improvements in setoid rewrite:Gravatar msozeau2008-08-27
| | | | | | | | | | | | | | | | | | - Avoid using projections for singleton classes. Divides the size of proofs by 2 and simplifies the typechecking as well. - Switch to the new discrimination net implementation for classes, with the current convention that all constants are unfoldable. Users can add "Typeclasses Opaque" declarations make the dnet discriminate more, otherwise it should be entirely backward-compatible. - Fix bug introduced in r11333 in "transitivity" tactic in presence of coercions. Up to 15% gains on setoid-intensive files like Ring_polynom and Field_theory. More importantly, performance should not decrease significantly by adding new Morphism/Setoid declarations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11337 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-01 21:09:26 +0000