aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/q_coqast.ml4
Commit message (Expand)AuthorAge
* A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> secondsGravatar letouzey2011-03-18
* Fix compilation with camlp5 (Closes: #2487)Gravatar glondu2011-01-25
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Extension of the recursive notations mechanismGravatar herbelin2010-07-22
* Add (almost) compatibility with camlp4, without breaking support for camlp5Gravatar letouzey2010-05-19
* static (and shared) camlp4use instead of per-file declarationGravatar letouzey2010-05-19
* Discontinue support for ocaml 3.09.*Gravatar letouzey2010-05-19
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* Only one "in" clause in "destruct" even for a multiple "destruct".Gravatar herbelin2009-09-20
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Added "etransitivity".Gravatar herbelin2009-08-03
* - Added two new introduction patterns with the following temptative syntaxes:Gravatar herbelin2009-06-07
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* About "apply in":Gravatar herbelin2008-12-09
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* A much better implementation of implicit generalization:Gravatar msozeau2008-10-22
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* - 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
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Modification rapide du message d'erreur lorsqu'un _ ne peut êtreGravatar herbelin2008-07-18
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveGravatar herbelin2008-04-25
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* - Relâchement de la contrainte de bonne longueur des intropatternsGravatar herbelin2008-04-04
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* * Adding compability with ocaml 3.10 + camlp5 (rework of Gravatar letouzey2007-09-15
* Generalized CAMLP4USE for pp dependenciesGravatar corbinea2007-07-16
* New bootstrapping, improved, Makefile systemGravatar corbinea2007-07-13
* New intro pattern "@A", which generates a fresh name based on A.Gravatar glondu2007-07-06
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Extension to the general sequence operator (tactical). Now in addition to ...Gravatar emakarov2007-04-02
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Exports manquants dans ringGravatar barras2006-10-29
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30