index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
elim.ml
Commit message (
Expand
)
Author
Age
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Fixing pervasive equalities. In particular, I removed the code that deleted
Pierre-Marie Pédrot
2014-03-03
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Modulification of identifier
ppedrot
2012-12-14
*
still some more dead code removal
letouzey
2012-10-06
*
remove Refiner.abstract_tactic and similar
letouzey
2012-10-06
*
Clean-up : removal of Proof_type.tactic_expr
letouzey
2012-10-06
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
Tacexpr as a mli-only, the few functions there are now in Tacops
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Cleaning/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
- Fixed bugs and compatibilities issues in
herbelin
2008-12-30
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
- Propagation des evars non résolues vers les with_bindings; permet par exemple
herbelin
2007-05-20
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Nouvelle en-tête
herbelin
2004-07-16
*
Déplacement définition intro_pattern_expr dans Genarg
herbelin
2004-03-01
*
Bug Double Inversion
herbelin
2003-10-27
*
Ajout option 'as [ ... ]' pour nommer les noms de 'Inversion'
herbelin
2003-10-10
*
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
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
code mort
herbelin
2003-04-07
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
Mise de Intros id au format de Intro en forçant aussi la réduction si demandé
herbelin
2002-01-15
*
compat ocaml 3.03
filliatr
2001-12-13
*
GROS COMMIT:
barras
2001-11-05
*
Suppression option immediate_discharge; nettoyage de Declare et conséquences
herbelin
2001-10-11
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
[next]