aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
Commit message (Expand)AuthorAge
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* commande Timeout + compaction des traces de debug_tacticGravatar barras2009-03-04
* Les records déclarés avec Record ne peuvent plus être récursifs (le Gravatar aspiwack2009-01-19
* Getting rid of the previous implementation of setoid_rewrite which wasGravatar 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
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Add user syntax for creating hint databases [Create HintDb fooGravatar msozeau2008-09-14
* Add the ability to declare [Hint Extern]'s with no pattern.Gravatar msozeau2008-09-07
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* 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
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Ajout d'abbréviations/notations paramétriquesGravatar herbelin2008-03-30
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Merge with lmamane's private branch:Gravatar lmamane2008-02-22
* 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
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* Modification of the Scheme command.Gravatar vsiles2007-09-28
* Modification of VernacScheme to handle a new scheme: Equality (equality inGravatar vsiles2007-05-25
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Nouveaux changements autour des implicites (notamment suite àGravatar herbelin2007-05-06
* New keyword "Inline" for Parameters and Axioms for automatic Gravatar soubiran2007-04-25
* Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)Gravatar herbelin2007-02-24
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 01:04:54 +0000