aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Collapse)AuthorAge
* New instance returns the (future) identifier of the instance.Gravatar msozeau2008-02-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10590 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
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
| | | | | | | | | | trying to declare an instance with an already existing name. Add possibility of not giving all the fields in Instance declarations, using Refine.refine to generate the subgoals. No control over opacity in this case though... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
| | | | | | | | | only, and get rid of the "relation" definition which makes unification fail blatantly. Replace it with a notation :) In its current state, the new tactic seems ready for larger tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10543 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
| | | | | | | | eauto instead of an arbitrary tactic. Export more from eauto to allow easier debugging. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10534 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add more information to IllFormedRecBody exceptions, to show the exactGravatar msozeau2008-02-08
| | | | | | | | definition on which it is failing (useful for Program definitions and others too). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10533 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backport code from command.ml to subtac_command.ml for defininingGravatar msozeau2008-02-08
| | | | | | | | | | recursive definitions. Now program accepts cofixpoints and uses the new way infer structurally decreasing arguments. Also, checks for correct recursive calls before giving the definition to the obligations machine (solves part 1 of bug #1784). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10529 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
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | kernel: -declaration.ml unification des representations pour les modules et modules types. (type struct_expr_body) -mod_typing.ml le typage des modules est separe de l'evaluation des modules -modops.ml nouvelle fonction qui pour toutes expressions de structure calcule sa forme evaluee.(eval_struct) -safe_typing.ml ajout du support du nouvel operateur Include.(add_include). library: -declaremods.ml nouveaux objets Include et Module-alias et gestion de la resolution de noms pour les alias via la nametab. parsing: -g_vernac.ml4: nouvelles regles pour le support des Includes et pour l'application des signatures fonctorielles. extraction: Adaptation a la nouvelle representation des modules et support de l'operateur with. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10497 85f007b7-540e-0410-9357-904b9bb8a0f7
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10484 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debug 0-ary typeclasses support, use new redefinition support for default tacticGravatar msozeau2008-01-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10482 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ↵Gravatar msozeau2008-01-18
| | | | | | | | | | wrapper around Ltac program_simpl ::= . !!!! This may introduce incompatibilities because now modifications of program_simpl are properly handled and work across modules. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10454 85f007b7-540e-0410-9357-904b9bb8a0f7
* Change notation for setoid inequality, coerce objects before comparing them. ↵Gravatar msozeau2008-01-18
| | | | | | Debug tactic redefinition code, streamline Instantiation Tactic implementation using that. Have to adapt obligations tactic still. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10449 85f007b7-540e-0410-9357-904b9bb8a0f7
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is ↵Gravatar msozeau2008-01-17
| | | | | | backwards compatible. Update CHANGES with things i've done. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Generalize instance declarations to any context, better name handling. Add ↵Gravatar msozeau2008-01-15
| | | | | | | | | hole kind info for topconstrs. Derive eta_expansion from functional extensionality axiom. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10439 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but ↵Gravatar msozeau2008-01-07
| | | | | | implementation is much less add-hoc. Opens possibility of arbitrary prefixes in Class and Instance declarations. Current implementation with eauto is a bit more dangerous... next patch will fix it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fixed bug 1761 (unexpected anomaly when constructor type has invalidGravatar herbelin2008-01-05
| | | | | | | | conclusion) and improved error message when the conclusion of the type of a constructor is invalid. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10425 85f007b7-540e-0410-9357-904b9bb8a0f7
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10416 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
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
| | | | | | | | | Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
* Print Assumptions est pret pour la release.Gravatar aspiwack2007-12-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10387 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
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
| | | | | | | | | | | | | - Le code est maintenant mieux commenté. - J'ai aussi réorganisé un petit peu pour le rendre plus léger, mais presque rien - j'ai changé les noms internes : needed_assumptions devient assumptions et PrintNeededAssumptions devient PrintAssumptions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10311 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des notations "alias" dans la globalisation des coercions.Gravatar herbelin2007-11-08
| | | | | | | | | | | | | | | | | | | | | | | | | Au passage, un peu plus de standardisation des noms de fonctions de globalisation Principe de base : locate_foo : qualid -> foo (échoue avec Not_found) global : reference -> global_reference (échoue avec UserError) global_of_foo : foo -> global_reference (échoue avec UserError) f_with_alias : se comporte comme f mais prenant aussi en compte les notations de la forme "Notation id:=ref" Principale exception : locate, au lieu de locate_global locate_global_with_alias, qui prend en entrée un "qualid located" Restent beaucoup de fonctions qui pourraient utiliser global_with_alias au lieu de global, notamment dans contribs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10305 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
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
| | | | | | | | | | | Printing Universes est active. Ajout de l'option "using" à la tactique non documentée "auto decomp". Ajout de la base "extcore" pour étendre "auto decomp" avec des principes élémentaires tels que le dépliage de "iff". Quelques extensions/raffinements dans ChoiceFacts et ClassicalFacts. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10156 85f007b7-540e-0410-9357-904b9bb8a0f7
* On Linux, we read /proc/self/exe to get the executable's path insteadGravatar glondu2007-09-28
| | | | | | | | of just relying on $0. This is needed, e.g. when coqtop -byte is being called via a link which is in $PATH, but coqtop.byte is not in $PATH. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10153 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of the Scheme command.Gravatar vsiles2007-09-28
| | | | | | | | | | | | Now you can forget to provide the name of the scheme, it will be built automatically depending of the sorts involved. e.g. Scheme Induction for nat Sort Set. will build nat_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10148 85f007b7-540e-0410-9357-904b9bb8a0f7
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
| | | | | | | | | | | | | | the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation politique de nommage evd/isevars (evd si evar_defs,Gravatar herbelin2007-09-06
| | | | | | | evdref si evar_defs ref) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10115 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise à jour des paramètres Whelp et ajouts d'options Set Whelp ServerGravatar herbelin2007-08-30
| | | | | | | | | et Set Whelp Getter pour changer le nom des serveurs (report 10105 de la 8.1 vers le trunk) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10106 85f007b7-540e-0410-9357-904b9bb8a0f7
* Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et ↵Gravatar herbelin2007-08-24
| | | | | | -rectypes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation plus précise de la contrainte de type pour interpréter lesGravatar herbelin2007-08-24
| | | | | | | | | | | points-fixes: on applique maintenant cette contrainte avant de généraliser corps et types vis à vis du context (utile notamment en présence de let-in dont on ne sait pas sinon s'ils font partie de la contrainte de type ou du contexte de typage). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification de l'initialisation des chemins de la librairie standardGravatar notin2007-08-20
| | | | | | | | | pour imposer un ordre précis des répertoires (résout en partie le problème entre Init.Wf et Program.Wf.) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10081 85f007b7-540e-0410-9357-904b9bb8a0f7
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
| | | | | | | Documented in dev/doc/build-system.txt . git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9992 85f007b7-540e-0410-9357-904b9bb8a0f7
* If a fixpoint is not written with an explicit { struct ... }, then Gravatar letouzey2007-07-07
| | | | | | | | | | | | | | | | | | | | | | | | all arguments are tried successively (from left to right) until one is found that satisfies the structural decreasing condition. When the system accepts a fixpoint, it now prints which decreasing argument was used, e.g: plus is recursively defined (decreasing on 1st argument) The search is quite brute-force, and may need to be optimized for huge mutual fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback. N.B. in the standard library, only 4 functions have an decreasing argument different from the one that would be automatically infered: List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind And compiling with as few explicit struct as possible would add about 15s in compilation time for the whole standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9961 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Ajout de la possibilité d'utiliser la notation Record pour lesGravatar herbelin2007-06-30
| | | | | | | | | | coinductifs à un constructeur (suggestion de Georges). - Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record, Type est utilisé comme défaut. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9917 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction d'un bug dans l'affichage du message d'erreur real_cleanGravatar herbelin2007-05-29
| | | | | | | | | (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type d'evar EvarGoal pour raffinement du message d'erreur. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contrôle de la compatibilité de apply via une information dans lesGravatar herbelin2007-05-28
| | | | | | | | métas permettant de savoir si une instance de méta vient d'un with-binding ou d'une unification, et si elle a déjà été typée ou pas. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9866 85f007b7-540e-0410-9357-904b9bb8a0f7
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
| | | | | | | | | | | | | | | | | boolean, will be added later) and update so everything is fine with the new syntax. New Type: type scheme = | InductionScheme of bool * lreference * sort_expr | EqualityScheme of lreference ... | VernacScheme of (lident * scheme) list git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage et standardisation des messages d'erreurs.Gravatar herbelin2007-05-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9831 85f007b7-540e-0410-9357-904b9bb8a0f7
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
| | | | | | | | | details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
| | | | | | | | | | | | | discussion avec Georges) - La notion d'insertion maximale n'est plus globale mais attachée à chaque implicite - Correction de petits bugs dans le calcul des implicites - Raffinement de la notion "sous contexte" pour l'affichage des coercions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9817 85f007b7-540e-0410-9357-904b9bb8a0f7
* Multiples changements autour des implicites :Gravatar herbelin2007-04-29
| | | | | | | | | | | | | | | | | | | | | | | | | | | | - correction du mode strict qui n'était pas si strict, - option "Set Strong Strict Implicit" pour activer le mode strictement strict (désactivé par défaut pour raison de compatibilité), - option "Set Reversible Pattern Implicit" pour activer les implicites inférables par unification-pattern (désactivé par défaut par compatibilité), - option "Unset Printing Implicit Defensive" pour désactiver l'affichage des implicites n'ayant pas été décelés stricts, - option "Set Maximal Implicit Insertion" pour que les applications soient saturées en implicites si possible, - une optimisation du mode non strict pour que l'algo de recherche des implicites renonce à calculer les occurrences non strictes qui pourraient avoir à être affichées dans le mode défensif, avec pour conséquence que le mode défensif, pour celui qui le veut, devient a priori encore plus verbeux, ex: Set Implicit Arguments. Definition id x : nat := x. Parameter f : forall n, id n = id n -> Prop. Check (f (refl_equal O)). (* Affichait: "f (refl_equal 0)" mais affiche maintenant "f (n:=0) (refl_equal 0)" *) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug #1507 (report révision 9807 de v8.1 vers trunk)Gravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9809 85f007b7-540e-0410-9357-904b9bb8a0f7
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | delta-reduction at fonctor application. Example: Module Type S. Parameter Inline N : Set. End S. Module F (X:S). Definition t := X.N. End F. Module M. Definition N := nat. End M. Module G := F M. Print G.t. G.t = nat : Set git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reorder hook and printing of message, more natural this way.Gravatar msozeau2007-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9782 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:36:28 +0000