aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_vernac.ml4
Commit message (Expand)AuthorAge
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* DISCLAIMERGravatar puech2009-01-17
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* - Standardized prefix use of "Local"/"Global" modifiers as decided inGravatar herbelin2009-01-13
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* - coq_makefile: target install now respects the original tree structureGravatar herbelin2008-12-24
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Fix mixup between Record, Structure and Class by adding a new variant forGravatar msozeau2008-11-10
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* Move Record desugaring to constrintern and add ability to use notationsGravatar msozeau2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Renommage "Global Instance" en "Instance Global" pour uniformisationGravatar herbelin2008-10-20
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Correct handling of implicit arguments in [Equations] definitions,Gravatar msozeau2008-09-03
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* - Correction de la version simplifiée (filtrage sur deux sigGravatar herbelin2008-06-09
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* - Changement du code de Zplus pour accomoder ring qui sinon prend uneGravatar herbelin2008-05-11
* Better parsing of typeclasses, any constr is allowed for ! bindings soGravatar msozeau2008-05-06
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* - Un peu de doc, préparation du CHANGES pour la release.Gravatar herbelin2008-04-15
* Chgts mineurs:Gravatar herbelin2008-04-03
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* fix the syntax "Include Type Foo"Gravatar letouzey2008-02-02
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Support for substructures in classes using :> notationGravatar msozeau2008-01-30
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* Modification of the Scheme command.Gravatar vsiles2007-09-28
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* Slight cleanup of refl_omega.ml : in particular it uses now listGravatar letouzey2007-07-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 06:36:39 +0000