aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacexpr.ml
Commit message (Expand)AuthorAge
* 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
* Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"Gravatar herbelin2009-03-16
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* About "apply in":Gravatar herbelin2008-12-09
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Correction de bugs:Gravatar herbelin2008-08-05
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Add possibility to match on defined hypotheses, using brackets toGravatar msozeau2008-06-16
* Correction de deux bugs liés au commit 11094 sur les clauses "at" et "in".Gravatar herbelin2008-06-11
* - 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
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Diverses corrections Gravatar herbelin2008-04-14
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* 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
* 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
* Suppression de code mortGravatar notin2007-02-01
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Suppression du type 'tac dans les abstract_argument_type: devenu inutile Gravatar herbelin2006-11-20
* Extension de la primitive ltac fresh pour qu'elle accepte une liste deGravatar herbelin2006-10-24
* 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
* Extension syntaxique de rewrite in: au lieu de pouvoir faire Gravatar letouzey2006-05-02
* + 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
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Extension de Tactic Notation pour permettre d'tendre et de faire rffrence aux...Gravatar herbelin2005-05-17
* Allow auto to have a parametric argument (wish #967)Gravatar herbelin2005-05-15
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Ajout constructeur External pour appel outil externe à CoqGravatar herbelin2005-02-04
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21