aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pcoq.mli
Commit message (Expand)AuthorAge
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Using vernac parsing for FunctionGravatar jforest2010-06-08
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* Nicer representation of tokens, more independant of camlp*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Fixed a little bug in previous commit (bad failure in case of unknown entry).Gravatar herbelin2009-04-27
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* Fixing/improving management of uniform prefix Local and GlobalGravatar herbelin2009-01-14
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* - Export de pattern_ident vers les ARGUMENT EXTEND and co.Gravatar herbelin2008-10-19
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Correction d'un autre bug autour de la gestion des niveaux vides deGravatar herbelin2008-07-11
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Résolution bug #1850 sur notations avec niveaux inconnus deGravatar herbelin2008-05-26
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Contournement laborieux de la "feature" de camlp5 qui entrainait leGravatar herbelin2008-04-30
* Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour Gravatar herbelin2008-04-26
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* 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
* Creation of a new token PATTERNIDENT (?ident) for intro patterns, soGravatar glondu2007-09-28
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* gestion speciale du niveau 5 des ltacGravatar barras2006-11-02
* Declarative Proof Language: main commitGravatar corbinea2006-09-20
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...Gravatar herbelin2006-01-09
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Added entry constr_may_eval for tactic extensions (new syntax)Gravatar herbelin2005-06-22
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17