aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pptactic.ml
Commit message (Expand)AuthorAge
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* - 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
* - Remove some dead code in subtacGravatar msozeau2008-09-02
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* 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
* Clarification de l'ordre d'interprétation des variables dans ltac. EnGravatar herbelin2008-05-01
* 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
* Typo affichage "simple apply"Gravatar herbelin2008-04-01
* Ajout "simple apply" et "simple eapply" pour apply sans unfoldGravatar herbelin2008-04-01
* f_equal, revert, specialize in ML, contradict in better Ltac (+doc)Gravatar letouzey2008-03-07
* Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As partGravatar msozeau2008-03-07
* Rework on rich forms of rewriteGravatar letouzey2008-03-01
* Unification de TacLetRecIn et TacLetIn. En particulier, on peutGravatar herbelin2008-02-01
* 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
* Ajout infos de débogage de "universe inconsistency" quand option SetGravatar herbelin2007-09-30
* Adding a syntax for "n-ary" rewrite: Gravatar letouzey2007-07-06
* extension of the rename tactic: the following is now allowed: Gravatar letouzey2007-07-06
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* 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
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* fixed field_simplify + changed precedence of let and fun in ltacGravatar barras2006-10-30
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
* Déplacement surround dans util.ml et parenthésage des déclarationsGravatar herbelin2006-09-23
* Changement du type d'argument 'TacticArgType X' en un typeGravatar herbelin2006-06-08
* Factorisation utilisation environnement dans make_pr_tacGravatar herbelin2006-06-08
* Correction trou de subject-reduction de create_arg dans genarg.mliGravatar herbelin2006-06-07
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* Diverses corrections de l'afficheur et du traducteur pour s'assurer deGravatar herbelin2006-04-26
* Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;Gravatar herbelin2006-04-24
* + destruct now works as induction on multiple arguments : Gravatar jforest2006-03-21
* induction now admits multiple induction arguments. The principle mustGravatar coq2006-02-10
* Ajout option 'using lemmas' à auto/trivial/eautoGravatar herbelin2006-01-28
* Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...Gravatar herbelin2006-01-21
* Ajout motif d'introduction "?" (IntroAnonymous) pour laisser CoqGravatar herbelin2006-01-16
* - Tactic "assert" now accepts "as" intro patterns and "by" tactic clausesGravatar herbelin2006-01-16
* cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"Gravatar herbelin2006-01-16
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11