index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
auto.ml
Commit message (
Expand
)
Author
Age
*
- 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
*
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
*
Ajout option 'using lemmas' à auto/trivial/eauto
herbelin
2006-01-28
*
Suppression code pour hints nommés à la V7 (voire à la V6...)
herbelin
2006-01-28
*
Suppression de la dépendance en Map.fold de ocaml dont la sémantique a
herbelin
2006-01-24
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
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
*
Adoption du nom canonique global_of_constr pour éviter confusion avec type r...
herbelin
2005-05-20
*
Allow auto to have a parametric argument (wish #967)
herbelin
2005-05-15
*
Standardisation of function names about global references (especially, renami...
herbelin
2005-02-18
*
HUGE COMMIT
sacerdot
2005-01-03
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
The type Pattern.constr_label was isomorphic to Libnames.global_reference.
sacerdot
2004-12-07
*
MAJ affichage nouvelle syntaxe
herbelin
2004-12-06
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
put empty_env in hint clause (vo were becoming huge!)
barras
2004-09-15
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
simplification de clenv
barras
2004-09-10
*
unification encore...
barras
2004-09-08
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
factorisation et generalisation des clauses
barras
2003-11-13
*
reorganisation des niveaux (ex: = est a 70)
barras
2003-10-22
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Ajout option Local à Hint, Hints et HintDestruct
herbelin
2003-06-14
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac; localisation des appels à des tactiques défi...
herbelin
2003-03-31
*
*** empty log message ***
barras
2003-03-12
*
Option pour rendre les vérifications du refiner optionnelle
herbelin
2002-12-09
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Vraie substitutivite de autohints
coq
2002-10-01
*
passage a ocaml 3.06
herbelin
2002-09-27
*
Renoncement à distinguer les types "constr" et "types"; nettoyage
herbelin
2002-08-13
*
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
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
substitution et pattern modulo let
barras
2002-02-11
*
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
*
Change la constante d'entree de Immediate
mohring
2001-08-28
[next]