index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
leminv.ml
Commit message (
Expand
)
Author
Age
*
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
*
Noise for nothing
pboutill
2012-03-02
*
Proof using ...
gareuselesinge
2011-12-12
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Revert "Add [Polymorphic] flag for defs"
msozeau
2011-04-13
*
Add [Polymorphic] flag for defs
msozeau
2011-04-13
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixed bug #2314 (inversion using not checking the correctness of its arguments
herbelin
2010-06-13
*
Fixing Derive Inversion for new proof engine
herbelin
2010-05-26
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Here comes the commit, announced long ago, of the new tactic engine.
aspiwack
2010-04-22
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Cleaning/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
pushed evar reduction in kernel
barras
2009-02-06
*
Uniformisation du format des messages d'erreur (commencent par une
herbelin
2008-07-17
*
Plus de combinateurs sont passés de Util à Option. Le module Options
aspiwack
2007-12-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
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Changement des named_context
gregoire
2005-12-02
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
unification encore...
barras
2004-09-08
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
Unification lemInv et lemInv_in
herbelin
2003-10-10
*
Utilisation du second-ordre avec possibilité de K-rédex dans lemInv
herbelin
2002-12-24
*
suite du commit precedent
barras
2002-12-19
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
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
*
compat ocaml 3.03
filliatr
2001-12-13
*
Suites modifs du noyau. Univ devient purement fonctionnel.
barras
2001-11-12
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
Suppression des arguments sur les constantes, inductifs et constructeurs
barras
2001-10-09
[next]