index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
Commit message (
Expand
)
Author
Age
*
Ajout d'un point d'entree pour exporter les arbres de preuves en XML
herbelin
2002-07-24
*
MAJ commentaires
herbelin
2002-07-23
*
Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...
herbelin
2002-07-11
*
Commentaires
herbelin
2002-06-14
*
Bug non vérification non redondance par Cut
herbelin
2002-06-13
*
Déplacement de proofs vers tactics
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Fichier des expressions de tactiques
herbelin
2002-05-29
*
Ajout de Eval, Inst et Check
delahaye
2002-05-27
*
Nouvelle syntaxe 'Match Reverse Context' pour garder un filtrage de
herbelin
2002-05-15
*
Finalement VTactic est gardé pour y plonger les tactiques ML, le
herbelin
2002-05-15
*
Contournement de la fermeture ML dans VContext
herbelin
2002-05-15
*
- Changement de l'ordre de filtrage dans "Match Context"
herbelin
2002-05-14
*
modification de clenv_merge:
barras
2002-05-14
*
typed unification in the case of Pattern
barras
2002-04-17
*
backtrack unification
barras
2002-04-12
*
q: Commande introuvable.
herbelin
2002-04-12
*
Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannion
herbelin
2002-04-12
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
backtrack dans l'algo d'unification
barras
2002-04-10
*
Simplification des Clear internes dégénérés (sans hypothèses à effacer)
herbelin
2002-04-10
*
resolution du pb d'efficacite du a Sign.add_named_decl
barras
2002-04-04
*
transformation des evar en meta preserve la linearite des metas
barras
2002-04-03
*
changement de l'undo limit
barras
2002-04-03
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
backtrack de l'unification
barras
2002-03-21
*
encore quelques petites modif de l'unification
barras
2002-03-20
*
Rétablissement de look_for_interp
delahaye
2002-03-18
*
Meilleure gestion de la reduction dans Field
delahaye
2002-03-17
*
Retablissement de interp_tab + injection id -> constr sans goal
delahaye
2002-03-12
*
Propagation du pb de conversion dans clenv_unify
herbelin
2002-03-12
*
renommage de fonctions
barras
2002-03-08
*
Clear ne substitue plus le corps dans le reste du but
barras
2002-03-07
*
unification faite de gauche a droite (et non pas l'inverse) pour eviter que
barras
2002-03-05
*
*** empty log message ***
barras
2002-03-04
*
Nouveau Rewrite-in plus economique
barras
2002-03-04
*
Uniformisation convert_hyp
herbelin
2002-02-28
*
Generalisation de l'utilisation de l'unification d'ordre 2
barras
2002-02-28
*
suppression de pop_named
barras
2002-02-22
*
code mort dans tactinterp; plus de Debug On/Off dans Correctness
filliatr
2002-02-21
*
petits changements cosmetiques sur les tactiques
barras
2002-02-15
*
- Reforme de la gestion des args recursifs (via arbres reguliers)
barras
2002-02-14
*
petite modif pour ne pas expanser trop de let pendant l'unification
barras
2002-02-12
*
prterm -> prterm_env
filliatr
2002-02-08
*
petit nettoyage de kernel/inductive
barras
2002-02-07
*
Ajout tactiques Rename et Pose; modifications pour Inversion
herbelin
2002-02-01
*
Convertibilité au lieu d'alpha-équivalence pour les motifs non linéaires d...
herbelin
2001-12-20
*
reparation de make doc (ocamlweb & _)
letouzey
2001-12-19
[next]