aboutsummaryrefslogtreecommitdiff
path: root/toplevel/metasyntax.mli
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-09-14Allowing to extend the Print Grammar command generically.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-03-20Moving the tactic related code from Metasyntax to a new file.Pierre-Marie Pédrot
2016-02-01Infering atomic ML entries from their grammar.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-27Indexing existentially quantified entries returned by interp_entry_name.Pierre-Marie Pédrot
2015-06-26Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Lionel Rieg
2015-01-12Update headers.Maxime Dénès
2014-09-29Notation: option to attach extra pretty printing rules to notationsEnrico Tassi
2014-07-27Qualified ML tactic names. The plugin name is used to discriminatePierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2012-12-14Modulification of identifierppedrot
2012-08-11Added support for option Local (at module level) in Tactic Notation.herbelin
2012-08-08Updating headers.herbelin
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-26Slight change in the semantics of arguments scopes: scopes can noherbelin
2012-03-20Continuing r15045-15046 and r15055 (fixing bug #2732 about atomicherbelin
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Simplified the way internalization_data (i.e. bindings of bound varsherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-14- Addition of "Reserved Infix" continued.herbelin
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-11Add support for "Infix ... := constr" instead of just "Infix ... := ref".herbelin
2009-04-27- Cleaning (unification of ML names, removal of obsolete code,herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-23Simplifification de vernac_expr li l'abandon du traducteurherbelin
2005-05-17Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...herbelin
2005-01-02Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...herbelin
2004-07-16Nouvelle en-têteherbelin
2003-11-22Traitement plus clair, notamment pour Locate, de quand quoter les composantes...herbelin
2003-10-14Changement 'as notation' en 'where notation'herbelin
2003-10-01Implantation de l'option 'format' des Notationsherbelin
2003-09-30Ajout 'Close Scope'.herbelin
2003-09-19parsingherbelin
2003-09-12Ajout 'Print Scopes' et 'Bind Scope with classes'herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:20:51 +0000