index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
hiddentac.ml
Commit message (
Expand
)
Author
Age
*
Applying Tom Prince's patch to support parametric "constructor n" in
herbelin
2011-10-25
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixed a bug in pretty-printing "induction" and "destruct" due to a
herbelin
2010-06-13
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Removing redundant internal variants of apply tactic and simplification of ML...
herbelin
2010-04-14
*
Fixing bug #2146 (broken selection of occurrences in "change").
herbelin
2009-12-30
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Only one "in" clause in "destruct" even for a multiple "destruct".
herbelin
2009-09-20
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
Fixed a typo in "info" for tactic "right".
herbelin
2009-08-02
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Fixing bug #2308 ("instantiate" tactic did not comply with
herbelin
2009-04-24
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
About "apply in":
herbelin
2008-12-09
*
Fix bug #1977 by allowing the [apply] variants to take an [open_constr]
msozeau
2008-10-23
*
Add a type argument to letin_tac instead of using casts and recomputing
msozeau
2008-09-12
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)
herbelin
2008-06-10
*
- Extension de "generalize" en "generalize c as id at occs".
herbelin
2008-06-08
*
Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve
herbelin
2008-04-25
*
Bugs, nettoyage, et améliorations diverses
herbelin
2008-04-13
*
Ajout "simple apply" et "simple eapply" pour apply sans unfold
herbelin
2008-04-01
*
f_equal, revert, specialize in ML, contradict in better Ltac (+doc)
letouzey
2008-03-07
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Ajout de eelim, ecase, edestruct et einduction (expérimental).
herbelin
2007-10-03
*
extension of the rename tactic: the following is now allowed:
letouzey
2007-07-06
*
Nouvelle stratégie d'unification des types des with-bindings dans
herbelin
2007-05-22
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.
herbelin
2007-04-28
*
Changement dans le kernel :
bgregoir
2006-12-11
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses
herbelin
2006-01-16
*
Added 'clear - id' to clear all hypotheses except the ones dependent in the s...
herbelin
2005-03-07
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
Nouvelle en-tête
herbelin
2004-07-16
*
more evar stuff
corbinea
2004-06-28
*
effective evar refining
corbinea
2004-06-26
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
bugs avec Pose et Assert
barras
2004-01-09
*
factorisation et generalisation des clauses
barras
2003-11-13
*
Added Instantiate ... in
corbinea
2003-11-06
*
changement nouvelle syntaxe (pt fixes)
barras
2003-10-10
*
Ajout 'Symmetry in Hyp'
herbelin
2003-06-19
*
Utilisation de intro_pattern dans NewDestruct/NewInduction
herbelin
2003-06-13
*
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
[next]