aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.common
Commit message (Collapse)AuthorAge
* A file that can be loaded when a migration from Set to Type is desiredGravatar letouzey2008-04-04
| | | | | | | | | | (for instance as a consequence of the Set/Type switch of a library such as FSets). After a "Require Export SetIsType.", Set becomes a mere notation for Type (I love notations !). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10757 85f007b7-540e-0410-9357-904b9bb8a0f7
* New file FMapFullAVL containing the balancing proofs about FMapAVL:Gravatar letouzey2008-04-03
| | | | | | | | | | | | | | As for FSetAVL vs. FSetFullAVL, preservation of the balancing of trees is not necessary anymore for just fulfilling the Map interface. But we still want theses proofs to exists somewhere, since they ensure the correct efficiency of the FMapAVL operations. In addition, FSetFullAVL also contains the non-structural, ocaml-faithful version of compare. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10748 85f007b7-540e-0410-9357-904b9bb8a0f7
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
| | | | | | | | | | | | | | | | | | | - Better interface in constrintern w.r.t. evars used during typechecking - Add "unsatisfiable_constraints" exception which gives back the raw evar_map that was not satisfied during typeclass search (presentation could be improved). - Correctly infer the minimal sort for typeclasses declared as definitions (everything was in type before). - Really handle priorities in typeclass eauto: goals produced with higher priority (lowest number) instances are tried before other of lower priority goals, regardless of the number of subgoals. - Change inverse to a notation for flip, now that universe polymorphic definitions are handled correctly. - Add EquivalenceDec class similar to SetoidDec, declaring decision procedures for equivalences. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10724 85f007b7-540e-0410-9357-904b9bb8a0f7
* Installation des .vo nécessaire à BigQGravatar notin2008-03-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10703 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of the old IntMap library from StdLib to a user contrib ↵Gravatar letouzey2008-03-19
| | | | | | (Cachan/IntMap) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout cible programs comme synonyme de subtacGravatar herbelin2008-03-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
| | | | | | | | | | | | implicits for left, inl or eq, hence some theories had to be changed again. It should make some user contribs compile again too. Also do not import functional extensionality when importing Program.Basics, add a Combinators file for proofs requiring it and a Syntax file for the implicit settings. Move Classes.Relations to Classes.RelationClasses to avoid name clash warnings as advised by Hugo and Pierre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10681 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganisation of FSetAVL (consequences of remarks by B. Gregoire)Gravatar letouzey2008-03-15
| | | | | | | | | | | | | | | | | | | * FSetAVL is greatly lightened : modulo a minor change in bal, formal proofs of avl invariant is not needed for building a functor implementing FSetInterface.S (even if this invariant is still true) * Non-structural functions (union, subset, compare, equal) are transformed into efficient structural versions * Both proofs of avl preservation and non-structural functions are moved to a new file FSetFullAVL, that can be ignored by the average user. Same for FMapAVL (still work in progress...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10679 85f007b7-540e-0410-9357-904b9bb8a0f7
* tactique Gappa : mise en placeGravatar filliatr2008-03-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
| | | | | | | | | | | | | | | | | | implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plug the new setoid implemtation in, leaving the original one commentedGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | out. The semantics of the old setoid are faithfully simulated by the new tactic, hence no scripts involving rewrite are modified. However, parametric morphism declarations need to be changed, but there are only a few in the standard library, notably in FSets. The declaration and the introduction of variables in the script need to be tweaked a bit, otherwise the proofs remain unchanged. Some fragile scripts not introducting their variable names explicitely were broken. Requiring Setoid requires Program.Basics which sets stronger implicit arguments on some constants, a few scripts benefit from that. Ring/field have been ported but do not really use the new typeclass architecture as well as they could. Performance should be mostly unchanged, but will certainly improve in the near future. Size of the vo's seems not to have changed at all. It will certainly break some contribs using Setoid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10631 85f007b7-540e-0410-9357-904b9bb8a0f7
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
| | | | | | | | | | (Axiom/Variable...). New tactic clapply to apply unapplied class methods in tactic mode, simple solution to the fact that apply does not work up-to classes yet. Add Functions.v for class definitions related to functional morphisms. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
| | | | | | | | | | - New vernac command "Delete" - New vernac command "Undo To" - Added a few hooks used by new contrib/interface - Beta/incomplete version of dependency generation and dumping git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petits oublis dans Makefile.docGravatar notin2008-02-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plongement de doc/Makefile dans la nouvelle architecutre des MakefileGravatar notin2008-02-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10570 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move class_setoid to class_tactics.Gravatar msozeau2008-02-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10564 85f007b7-540e-0410-9357-904b9bb8a0f7
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
| | | | | | | | | | | | | | | | | | | | | Tabareau: - first pass: generation of the Morphism constraints with metavariables for unspecified relations by one fold over the term. This builds a "respect" proof term for the whole term with holes. - second pass: constraint solving of the evars, taking care of finding a solution for all the evars at once. - third step: normalize proof term by found evars, apply it, done! Works with any relation, currently not as efficient as it could be due to bad handling of evars. Also needs some fine tuning of the instances declared in Morphisms.v that are used during proof search, e.g. using priorities. Reorganize Classes.* accordingly, separating the setoids in Classes.SetoidClass from the general morphisms in Classes.Morphisms and the generally applicable relation theory in Classes.Relations. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10515 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorganization of FSet+FMap : no more files specific to Weak Sets/MapsGravatar letouzey2008-02-04
| | | | | | | | | | | | | | | | | Thanks to Elie's work and especially "Include Type ...", full sets can be simply expressed as extensions of weak sets. Moreover, Facts and Properties functors can be factorized almost completely. As a result, things like FSetWeakAAA.BBB can now be found as FSetAAA.WBBB, Same with maps / weak maps ... No backward compatibility intended for weak sets / maps, but porting scripts should mostly amounts to name changes (see above). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10505 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
| | | | | | | | | | | | | | | | | | for basic functional programming and relation definitions respectively. Classes.Relations also includes the definition of Morphism and instances for the standard morphisms and relations (eq, iff, impl, inverse and complement). The class_setoid.ml4 [setoid_rewrite] tactic has been reimplemented on top of these definitions, hence it doesn't require a setoid implementation anymore. It also generates obligations for missing reflexivity proofs, like the current setoid_rewrite. It has not been tested on large examples but it should handle directions and occurences. Works with in if no obligations are generated at this time. What's missing is being able to rewrite by a lemma instead of a simple hypothesis with no premises. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10502 85f007b7-540e-0410-9357-904b9bb8a0f7
* factorization part II (Properties + EqProperties), inclusion of FSetDecide ↵Gravatar letouzey2008-02-02
| | | | | | (from A. Bohannon) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10500 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prove the decidability of arithmetical statements using the real numbers.Gravatar roconnor2008-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10473 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10447 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug in sqrt321Gravatar thery2008-01-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10444 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration de la génération des graphes de dépendancesGravatar notin2008-01-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10438 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add partial setoids in theories/Classes, add SetoidDec class for setoids ↵Gravatar msozeau2008-01-04
| | | | | | with a decidable equality. Fix name capture bug, again. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10419 85f007b7-540e-0410-9357-904b9bb8a0f7
* Move Classes.Setoid to Classes.SetoidClass to avoid name clash.Gravatar msozeau2007-12-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10411 85f007b7-540e-0410-9357-904b9bb8a0f7
* Merged revisions ↵Gravatar msozeau2007-12-31
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,10398,10403-10408 via svnmerge from svn+ssh://msozeau@scm.gforge.inria.fr/svn/coq/branches/TypeClasses ........ r10358 | msozeau | 2007-12-10 15:42:53 +0100 (Mon, 10 Dec 2007) | 1 line Comment grammar error ........ r10359 | msozeau | 2007-12-10 16:04:09 +0100 (Mon, 10 Dec 2007) | 7 lines The initial Type Classes patch. This patch introduces type classes and instance definitions a la Haskell. Technically, it uses the implicit arguments mechanism which was extended a bit. The patch also introduces a notation for explicitely marking implicit, maximally inserted parameters. It includes the tactic redefinition code too (Ltac tac ::= foo redefines tac). ........ r10360 | msozeau | 2007-12-10 16:14:30 +0100 (Mon, 10 Dec 2007) | 1 line Fix interface ........ r10361 | msozeau | 2007-12-10 16:28:19 +0100 (Mon, 10 Dec 2007) | 1 line Fix more xlate code ........ r10362 | msozeau | 2007-12-11 02:00:53 +0100 (Tue, 11 Dec 2007) | 3 lines Update coqdoc for type classes, fix proof state not being displayed on Next Obligation. ........ r10365 | msozeau | 2007-12-11 14:22:35 +0100 (Tue, 11 Dec 2007) | 3 lines Bug fixes in Instance decls. ........ r10371 | msozeau | 2007-12-12 21:17:30 +0100 (Wed, 12 Dec 2007) | 3 lines Streamline typeclass context implementation, prepare for class binders in proof statements. ........ r10372 | msozeau | 2007-12-12 22:03:38 +0100 (Wed, 12 Dec 2007) | 1 line Minor cosmetic fixes: allow sorts as typeclass param instances without parens and infer more types in class definitions ........ r10373 | msozeau | 2007-12-13 00:35:09 +0100 (Thu, 13 Dec 2007) | 2 lines Better names in g_vernac, binders in Lemmas and Context [] to introduce a typeclass context. ........ r10377 | msozeau | 2007-12-13 18:34:33 +0100 (Thu, 13 Dec 2007) | 1 line Stupid bug ........ r10383 | msozeau | 2007-12-16 00:04:48 +0100 (Sun, 16 Dec 2007) | 1 line Bug fixes in name handling and implicits, new syntax for using implicit mode in typeclass constraints ........ r10384 | msozeau | 2007-12-16 15:53:24 +0100 (Sun, 16 Dec 2007) | 1 line Streamlined implementation of instances again, the produced typeclass is a typeclass constraint. Added corresponding implicit/explicit behaviors ........ r10394 | msozeau | 2007-12-18 23:42:56 +0100 (Tue, 18 Dec 2007) | 4 lines Various fixes for implicit arguments, new "Enriching" kw to just enrich existing sets of impl args. New syntax !a to force an argument, even if not dependent. New tactic clrewrite using a setoid typeclass implementation to do setoid_rewrite under compatible morphisms... very experimental. Other bugs related to naming in typeclasses fixed. ........ r10395 | msozeau | 2007-12-19 17:11:55 +0100 (Wed, 19 Dec 2007) | 3 lines Progress on setoids using type classes, recognize setoid equalities in hyps better. Streamline implementation to return more information when resolving setoids (return the results setoid). ........ r10398 | msozeau | 2007-12-20 10:18:19 +0100 (Thu, 20 Dec 2007) | 1 line Syntax change, more like Coq ........ r10403 | msozeau | 2007-12-21 22:30:35 +0100 (Fri, 21 Dec 2007) | 1 line Add right-to-left rewriting in class_setoid, fix some discharge/substitution bug, adapt test-suite to latest syntax ........ r10404 | msozeau | 2007-12-24 21:47:58 +0100 (Mon, 24 Dec 2007) | 2 lines Work on type classes based rewrite tactic. ........ r10405 | msozeau | 2007-12-27 18:51:32 +0100 (Thu, 27 Dec 2007) | 2 lines Better evar handling in pretyping, reorder theories/Program and add some tactics for dealing with subsets. ........ r10406 | msozeau | 2007-12-27 18:52:05 +0100 (Thu, 27 Dec 2007) | 1 line Forgot to add a file ........ r10407 | msozeau | 2007-12-29 17:19:54 +0100 (Sat, 29 Dec 2007) | 4 lines Generalize usage of implicit arguments in terms, up to rawconstr. Binders are decorated with binding info, either Implicit or Explicit for rawconstr. Factorizes code for typeclasses, topconstrs decorations are Default (impl|expl) or TypeClass (impl|expl) and implicit quantification is resolve at internalization time, getting rid of the arbitrary prenex restriction on contexts. ........ r10408 | msozeau | 2007-12-31 00:58:50 +0100 (Mon, 31 Dec 2007) | 4 lines Fix parsing of subset binders, bugs in subtac_cases and handling of mutual defs obligations. Add useful tactics to Program.Subsets. ........ git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10410 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction du bug #1745 (installation des fichiers .vo de Numbers)Gravatar notin2007-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10392 85f007b7-540e-0410-9357-904b9bb8a0f7
* migration of ide/utf8.v to theories/Unicode/Utf8.vGravatar letouzey2007-12-13
| | | | | | | | | | | | | | | | | | These notations aren't CoqIDE-specific, I can now use them with ProofGeneral (after a small modification of PG, contact me if you're interested by the patch). So let's place this file in a globally visible subdir of theories/. By the way, the filename is now uppercase as all other .v files. By the way, minor other changes in Makefile : extraction/test doesn't exist anymore, and tags / otags can be made without re-doing any find. NB: be sure to use etags that comes from emacs and not the one of exuberant-ctags, since the latter has now a different syntax (in debian, see update-alternatives etags). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10376 85f007b7-540e-0410-9357-904b9bb8a0f7
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
| | | | | | | | | devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
| | | | | | | | | | | | | | | | | | | | | | | | | | | lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting des fonctions (à un ou deux arguments tous ou partie de type option). Il reste quelques opérations dans Util à propos desquelles je ne suis pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain car il est tard (comme some_in qui devrait devenir Option.make je suppose) . Elles s'expriment souvent facilement en fonction des autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y" . Le option_cons devrait faire son chemin dans le module parce qu'il est assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml. J'en ai profité aussi pour remplacer les trop nombreux "failwith" par des erreurs locales au module, donc plus robustes. J'ai trouvé aussi une fonction qui était définie deux fois, et une définie dans un module particulier. Mon seul bémol (mais facile à traiter) c'est la proximité entre le nom de module Option et l'ancien Options. J'ai pas de meilleure idée de nom à l'heure qu'il est, ni pour l'un, ni pour l'autre. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added theorems; created NZPlusOrder from NTimesOrder.Gravatar emakarov2007-11-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10325 85f007b7-540e-0410-9357-904b9bb8a0f7
* Split NTimesOrder into properly NTimesOrder and NPlusOrder.Gravatar emakarov2007-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10324 85f007b7-540e-0410-9357-904b9bb8a0f7
* Update on Numbers; renamed ZOrder.v to ZLt to remove clash with ↵Gravatar emakarov2007-11-14
| | | | | | ZArith/Zorder on MacOS. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10323 85f007b7-540e-0410-9357-904b9bb8a0f7
* setoid_ring/Ring_zdiv is moved to ZArith and renamed to ZOdiv_def. Gravatar letouzey2007-11-08
| | | | | | | | | | | | | | A file ZOdiv is added which contains results about this euclidean division. Interest compared with Zdiv: ZOdiv implements others (better?) conventions concerning negative numbers, in particular it is compatible with Caml div and mod. ZOdiv is only partially finished... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10302 85f007b7-540e-0410-9357-904b9bb8a0f7
* Forgot a backslash in Makefile.common. Added "(only parsing)" in BinNat.v.Gravatar emakarov2007-11-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10299 85f007b7-540e-0410-9357-904b9bb8a0f7
* Replaced BinNat with a new version that is based on ↵Gravatar emakarov2007-11-07
| | | | | | theories/Numbers/Natural/Binary/NBinDefs. Most of the entities in the new BinNat are notations for the development in Numbers. Also added min and max to the new natural numbers and integers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10298 85f007b7-540e-0410-9357-904b9bb8a0f7
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension ↵Gravatar letouzey2007-11-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | of Zdiv Some details: - ZAux.v is the only file left in Ints/Z. The few elements that remain in it are rather specific or compatibility oriented. Others parts and files have been either deleted when unused or pushed into some place of ZArith. - Ints/List/ is removed since it was not needed anymore - Ints/Tactic.v disappear: some of its tactic were unused, some already in Tactics.v (case_eq, f_equal instead of eq_tac), and the nice contradict has been added to Tactics.v - Znumtheory inherits lots of results about Zdivide, rel_prime, prime, Zgcd, ... - A new file Zpow_facts inherits lots of results about Zpower. Placing them into Zpower would have been difficult with respect to compatibility (import of ring) - A few things added to Zmax, Zabs, Znat, Zsqrt, Zeven, Zorder - Adequate adaptations to Ints/num/* (mainly renaming of lemmas) Now, concerning Zdiv, the behavior when dividing by a negative number is now fully proved. When this was possible, existing lemmas has been extended, either from strictly positive to non-zero divisor, or even to arbitrary divisor (especially when playing with Zmod). These extended lemmas are named with the suffix _full, whereas the original restrictive lemmas are retained for compatibility. Several lemmas now have shorter proofs (based on unicity lemmas). Lemmas are now more or less organized by themes (division and order, division and usual operations, etc). Three possible choices of spec for divisions on negative numbers are presented: this Zdiv, the ocaml approach and the remainder-always-positive approach. The ugly behavior of Zopp with the current choice of Zdiv/Zmod is now fully covered. A embryo of division "a la Ocaml" is given: Odiv and Omod. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10291 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Adding BigQ and proofsGravatar thery2007-10-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10265 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added NIso.v to Makefile.common. Changed Examples.v in contrib/micromega to ↵Gravatar emakarov2007-10-25
| | | | | | use NRing instead of Ring_polynom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10264 85f007b7-540e-0410-9357-904b9bb8a0f7
* Intallation des .cma/.cmxaGravatar notin2007-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10241 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copie de PreOmega.vo dans le répertoire d'installation de CoqGravatar notin2007-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10239 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo dans Makefile.commonGravatar notin2007-10-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10237 85f007b7-540e-0410-9357-904b9bb8a0f7
* Major reorganisation of the extraction "backend".Gravatar letouzey2007-10-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Initial Idea: getting rid of nasty renaming issues in modules, in particular bugs #820 (part d) #1340 #1526 #1654 Final effect: lots of changes, simplifications, cleanups, unrelated fixes and ehancements, and also probably some regressions (time will tell). A few details: * no more experimental "Toplevel" language. * no more functors Make in Ocaml/Haskell/Scheme. The spirit of these functors and Mlpp_params was already not followed much, and this framework was more a nuisance that anything else. * instead, some records language_descr regrouping the specific features of the different output languages. * Common now comes before Ocaml/Haskell/Scheme, these ones are now independant from each others. print_structure_to_file is now in Extract_env. * A nice detail: no more duplications of warnings concerning axioms. * In modular extraction, the clashes due to the opened modules are now computed once and for all thanks to record_contents_fstlev, instead of re-asking Coq each time about these opened modules and using Extraction.constant_kind * some utilities about modules_path added and/or moved from Modutil to Table. * using a .v file as a module, e.g. in a functor application should now works in modular extraction. Now concerning renaming issues themselves: * printing is done twice, the first time toward /dev/null, in order to encounter the naming issues unsolvable by a simple qualification. On the second run, we create artificial modules Coq__123 for allowing qualification of these hidden objects. * names are now fully separated into their syntaxic categories: terms/types/constructors/modules * Only one last unsupported situation (but at least detected and signaled by an error): an object M.t from an external file-module M.v can't be printed when a local module M is in the way. This situation is really unlikely (in Coq you must use _long_ file-module name, e.g. Init.Datatypes.nat). It could be solved by inserting "module Coq_123 = M" at the beginning of the file, but then the signature of Coq_123 (that is, the one of M) should be written explicitely in the .mli, which is _really_ not nice. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10232 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allow a few build system optimisations/corner-cuttingGravatar lmamane2007-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
| | | | | | | | | | | | | | | | | | | | | | | | decidability of the usual equality Major changes: * andb_prop & andb_true_intro have been moved from Bool.v to Datatypes.v * added 2 files: * toplevel/ind_tables.ml* : tables where the boolean eqs and the decidability proofs are stored * toplevel/auto_ind_decl.ml* : code of the schemes that are automatically generated from inductives types (currently boolean eq & decidability ) * improvement of injection: if the decidability have been correctly computed, injection can now break the equalities over dependant pair How to use: Set Equality Scheme. to set the automatic generation of the equality when you create a new inductive type Scheme Equality for I. tries to create the equality for the already declared type I git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10180 85f007b7-540e-0410-9357-904b9bb8a0f7
* Added the proof (in Numbers/Integers/TreeMod) that tree-like representation ↵Gravatar emakarov2007-10-04
| | | | | | of integers due to Gregoire and Théry satisfies the axioms of integers without order. This refers to integers modulo n, i.e., those that fit trees of certain size, not to BigZ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10178 85f007b7-540e-0410-9357-904b9bb8a0f7
* Révision de theories/Logic concernant les axiomes de descriptions.Gravatar herbelin2007-10-03
| | | | | | | | Mise à jour du tableau des axiomes dans la FAQ. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10170 85f007b7-540e-0410-9357-904b9bb8a0f7
* The following now compiles: abstract integers with plus, minus and times, ↵Gravatar emakarov2007-10-02
| | | | | | binary implementation and integers as pairs of natural numbers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10167 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 19:10:04 +0000