aboutsummaryrefslogtreecommitdiff
path: root/parsing/q_coqast.ml4
AgeCommit message (Expand)Author
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
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-05-29Glob_term now mli-only, operations now in Glob_opsletouzey
2012-05-29Tacexpr as a mli-only, the few functions there are now in Tacopsletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-04-12"A -> B" is a notation for "forall _ : A, B".pboutill
2012-03-30info_trivial, info_auto, info_eauto, and debug (trivial|auto)letouzey
2012-03-02Noise for nothingpboutill
2012-01-30Added an pattern / occurence syntax for vm_compute.ppedrot
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-10-25Applying Tom Prince's patch to support parametric "constructor n" inherbelin
2011-03-18A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsletouzey
2011-01-25Fix compilation with camlp5 (Closes: #2487)glondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-22Extension of the recursive notations mechanismherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-19static (and shared) camlp4use instead of per-file declarationletouzey
2010-05-19Discontinue support for ocaml 3.09.*letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-12-30Fixing bug #2146 (broken selection of occurrences in "change").herbelin
2009-09-20Only one "in" clause in "destruct" even for a multiple "destruct".herbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-10Added syntax "exists bindings, ..., bindings" for iterated "exists".herbelin
2009-08-03Added "etransitivity".herbelin
2009-06-07- Added two new introduction patterns with the following temptative syntaxes:herbelin
2008-12-28- Another bug in get_sort_family_of (sort-polymorphism of constants andherbelin
2008-12-09About "apply in":herbelin
2008-10-26Fixes and refinements regarding occurrence selection:herbelin
2008-10-22A much better implementation of implicit generalization:msozeau
2008-10-22Affichage des notations récursives:herbelin
2008-10-19- Export de pattern_ident vers les ARGUMENT EXTEND and co.herbelin
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-08-05Correction de bugs:herbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-18Modification rapide du message d'erreur lorsqu'un _ ne peut êtreherbelin
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-16Add possibility to match on defined hypotheses, using brackets tomsozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-14Diverses corrections herbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-04- Relâchement de la contrainte de bonne longueur des intropatternsherbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-02-01Unification de TacLetRecIn et TacLetIn. En particulier, on peutherbelin
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau