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
...
*
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
*
Transparent
barras
2001-09-20
*
Remplacement de 'clause' par 'hyps' pour les tactiques qui ne peuvent pas s'a...
herbelin
2001-08-05
*
Branchement sur bad_tactic_args
herbelin
2001-07-10
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Prise en compte des noms longs dans les Hints et les Coercions, et réorganis...
herbelin
2001-01-24
*
conflit useInversionLemma
mohring
2000-12-13
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
caractere opaque des constantes repris en compte
filliatr
2000-12-04
*
nouveau discharge fait par le noyau; plus de recettes dans les corps des cons...
filliatr
2000-11-06
*
correction Abstract (et make world passe!)
filliatr
2000-11-02
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Abstraction de constr
herbelin
2000-09-14
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Extension de find_inductive aux co-inductifs et renommage en find_rectype
herbelin
2000-07-01
*
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-22
*
Nettoyage
herbelin
2000-05-18
*
Rien
herbelin
2000-05-16
*
Intégration de leminv
herbelin
2000-05-05
*
Intégration progressive
herbelin
2000-04-30
*
Inversion (pas termine)
filliatr
2000-03-27
[prev]