aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hiddentac.mli
Commit message (Expand)AuthorAge
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Fixing bug #2146 (broken selection of occurrences in "change").Gravatar herbelin2009-12-30
* In "simpl c" and "change c with d", c can be a pattern.Gravatar herbelin2009-12-24
* Generic support for open terms in tacticsGravatar herbelin2009-12-21
* 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
* - Add more precise error localisation when one of the application failsGravatar herbelin2009-08-04
* Added "etransitivity".Gravatar herbelin2009-08-03
* Fixing bug #2308 ("instantiate" tactic did not comply withGravatar herbelin2009-04-24
* About "apply in":Gravatar herbelin2008-12-09
* Fixes and refinements regarding occurrence selection:Gravatar herbelin2008-10-26
* Fix bug #1977 by allowing the [apply] variants to take an [open_constr]Gravatar msozeau2008-10-23
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* - 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
* 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
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* 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é d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* Changement dans le kernel : Gravatar bgregoir2006-12-11
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* + 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 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
* Added 'clear - id' to clear all hypotheses except the ones dependent in the s...Gravatar herbelin2005-03-07
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...Gravatar herbelin2005-01-02
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* more evar stuffGravatar corbinea2004-06-28
* effective evar refiningGravatar corbinea2004-06-26
* Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id va...Gravatar herbelin2004-03-02
* Déplacement définition intro_pattern_expr dans GenargGravatar herbelin2004-03-01
* bugs avec Pose et AssertGravatar barras2004-01-09
* Uniformisation des politiques de nommage de NewDestruct sur arguments recursi...Gravatar herbelin2003-11-25
* factorisation et generalisation des clausesGravatar barras2003-11-13
* Added Instantiate ... inGravatar corbinea2003-11-06
* changement nouvelle syntaxe (pt fixes)Gravatar barras2003-10-10
* Ajout 'Symmetry in Hyp'Gravatar herbelin2003-06-19
* Utilisation de intro_pattern dans NewDestruct/NewInductionGravatar herbelin2003-06-13