aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
Commit message (Collapse)AuthorAge
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
| | | | | | | | | | | | | - Backtrack on precise unfolding of "iff" in "tauto": it has effects on the naming of hypotheses (especially when doing "case H" with H of type "{x|P<->Q}" since not unfolding will eventually introduce a name "i" while unfolding will eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a plugin is missing, doc hnf, standardization of names manipulating type constr_pattern, ...). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
| | | | | | | | | | | | | of the archive to install in coq user-contrib installation directory. - Relaxed the validity check on identifiers from an error to a warning. - Added a filtering option to Print LoadPath. - Support for empty root in option -R. - Better handling of redundant paths in ml loadpath. - Makefile's: Added target initplugins and added initplugins to coqbinaries. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11713 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 mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
| | | | | | | the three cases. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11572 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
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
| | | | | | | | | for record fields (using "someproj : sometype where not := constr" syntax). Only one notation allowed currently and no redeclaration after the record declaration either (will be done for typeclasses). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11542 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
| | | | | | | | | | | | | | | | | | | | CoInductive stream (A:Type) := { hd : A ; tl : stream A }. Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }. L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de la syntaxe qui était apparue dans la 8.2beta pour les records coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" comme maintenant). VernacRecord et VernacInductive semblent maintenant faire doublon, il doit y avoir moyen de les fusionner. Les records mutuellement inductifs restent aussi à faire. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
| | | | | | | de l'utilisation des modificateurs Global/Local git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11480 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
| | | | | | | | | | | | - Extension du test de réversibilité acyclique des notations dures aux notations de type abbréviation (du genre inhabited A := A). - Ajout options Local/Global à Transparent/Opaque. - Retour au comportement 8.1 pour "move" (dependant par défaut et mot-clé dependent retiré). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11472 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
| | | | | | | | SearchAbout + referring objects by their notation). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11446 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
| | | | | | | | support for "where" notation declarations as well. Better checking of recursivity or not, after type-checking. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11354 85f007b7-540e-0410-9357-904b9bb8a0f7
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
| | | | | | | | | | majuscule - si pas un ident ou un terme - et se terminent par un point). Restent quelques utilisations de "error" qui sont liées à des usages internes, ne faudrait-il pas utiliser des exceptions plus spécifiques à la place ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11230 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
| | | | | | | | | | | | | | | classes, and simplify the implementation. - Experimental syntax {{ cl : Class args }} and (( cl : Class args )) which respectively make cl an implicit or explicit argument ({{ }} is equivalent to [ ]). Could be extended to any type of binder, eg. [Definition flip ((R : relation carrier)) : relation carrier := ...]. The idea behind double brackets is to distinguish macro-binders which perform implicit generalization from regular binders. It could also save [ ] for other uses. - Fix bug #1901 about {} binders in records. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11210 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
| | | | | | | | | | imbriqués) du bug 1834, mais le bug 1834 reste ouvert [cases.ml]. - Réactivation de l'interprétation des listes dans "generalize" cassée depuis 11072) [tacinterp.ml]. - Bricoles et petit nettoyage en passant [cases.ml et g_vernac.ml4]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
| | | | | | | | | | | | | | | | | | | | | | | files, about definitions and type of references. - Add missing location information on fixpoints/cofixpoint in topconstr and syntactic definitions in vernacentries for correct dumping. - Dump definition information in vernacentries: defs, constructors, projections etc... - Modify coqdoc/index.mll to use this information instead of trying to scan the file. - Use the type information in latex output, update coqdoc.sty accordingly. - Use the hyperref package to do crossrefs between definition and references to coq objects in latex. Next step is to test and debug it on bigger developments. On the side: - Fix Program Let which was adding a Global definition. - Correct implicits for well-founded Program Fixpoints. - Add new [Method] declaration kind. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
* Strategy commands are now exportedGravatar barras2008-05-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
* refined the conversion oracleGravatar barras2008-05-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
| | | | | | | | | | | | | | | | | | | change the default pretty-printing to use Π, λ instead of forall and fun (and allow "," as well as "=>" for "fun" to be more consistent with the standard forall and exists syntax). Parsing allows theses new forms too, even if not in -unicode, and does not make Π or λ keywords. As usual, criticism and suggestions are welcome :) Not sure what to do about "->"/"→" ? - [setoid_replace by] now uses tactic3() to get the right parsing level for tactics. - Type class [Instance] names are now mandatory. - Document [rewrite at/by] and fix parsing of occs to support their combination. - Backtrack on [Enriching] modifier, now used exclusively in the implementation of implicit arguments. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10921 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
| | | | | | | | | | | | | | binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
| | | | | | | | | | | | | | | complexité exponentielle dans la machine lazy depuis que l'algo de compilation du filtrage évite systématiquement d'expanser quand le filtrage n'est pas dépendant. - Un peu plus de colorisation dans coqide. - Utilisation de formats pour améliorer de l'affichage des notations Utf8. - Systématisation paire Local/Global dans g_vernac.ml4 (même si le défaut n'est pas toujours le même) - Bug Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10918 85f007b7-540e-0410-9357-904b9bb8a0f7
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
| | | | | | | notations work and bug #1846 gets completely fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10890 85f007b7-540e-0410-9357-904b9bb8a0f7
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
| | | | | | | | | | | | | | | | | | | name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
| | | | | | | | | | | des théorèmes prouvés par récursion ou corécursion mutuelle. Correction au passage du parsing et du printing des tactiques fix/cofix et documentation de ces tactiques. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10850 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
| | | | | | | | | | | | semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
| | | | | | | | | | | | | | | | - Re-restriction de inversion (après la correction des bugs - et notamment du "Unknown meta" qui apparaissait parfois -, inversion devenait capable d'agir sur des buts non atomiques, ce qui crée quelques incompatibilités, typiquement dans CoRN où inversion est utilisé dans un rôle de discriminate; en attendant de voir, on revient à la sémantique initiale). - Généralisation de Local/Global dans Implicit Arguments pour avoir un fonctionnement plus uniforme et plus facile à documenter. - Code mort (clenv.ml). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgts mineurs:Gravatar herbelin2008-04-03
| | | | | | | | | | - correction commit incorrect d'une modif de test-suite/success/apply.v - réorganisation dev/ - renommage Print Modules en Print Libraries - $Id:$ dans g_vernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10744 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
| | | | | | | | Example: "Notation reflexive R := (forall x, R x x)." git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10730 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
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
| | | | | | | | | | | | | | types. Change (again) the semantics of bindings and the binding modifier ! in typeclasses. Inside [ ], implicit binding where only parameters need to be given is the default, use ! to use explicit binding, which is equivalent to regular bindings except for generalization of free variables. Outside brackets (e.g. on the right of instance declarations), explicit binding is the default, and implicit binding can be used by adding ! in front. This avoids almost every use of ! in the standard library and in other examples I have. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10713 85f007b7-540e-0410-9357-904b9bb8a0f7
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
| | | | | | | | | | | | | | | | | | | | | binding, add "!" syntax for the new binders which require parameters and not superclasses. Change backquotes for curly braces for user-given implicit arguments, following tradition. This requires a hack a la lpar-id-coloneq. Change ident to global for typeclass names in class binders. Also requires a similar hack to distinguish between [ C t1 tn ] and [ c : C t1 tn ]. Update affected theories. While hacking the parsing of { wf }, factorized the two versions of fix annotation parsing that were present in g_constr and g_vernac. Add the possibility of the user optionaly giving the priority for resolve and exact hints (used by type classes). Syntax not fixed yet: a natural after the list of lemmas in "Hint Resolve" syntax, a natural after a "|" after the instance constraint in Instance declarations (ex in Morphisms.v). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10628 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
* fix the syntax "Include Type Foo"Gravatar letouzey2008-02-02
| | | | | | | | | I dont precisely understand what's going on, but it definitively works better after my fix (copied from the Module / Module Type settings). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10501 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
* 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
* 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
* 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
* 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
* 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
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
| | | | | | | | Removed parsing/lexer.ml4 special case No file depends on pa_extend_m.cmo anymore, Wierd ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10007 85f007b7-540e-0410-9357-904b9bb8a0f7
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
| | | | | | | | | utilities from Util. Some additions in Util, and simplifications in various files. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9969 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
* 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
* 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
* Suite commit 9810Gravatar herbelin2007-04-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9811 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout possibilité d'options à trois mots.Gravatar herbelin2007-04-29
| | | | | | | | | | Suppression au passage syntaxe "Set table field ref", synonyme de "Add table field ref" et de "Unset table field ref", synonyme de "Remove table field ref". Changement de la syntaxe "Test tabel field val" en ""Test tabel field for val". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9810 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 06:11:48 +0000