index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
refiner.ml
Commit message (
Expand
)
Author
Age
*
affichage des ... dans les scripts
barras
2006-10-16
*
revision de la semantique de rewrite ... in <clause>. details dans la doc
letouzey
2006-10-05
*
mise a jour du nouveau ring et ajout du nouveau field, avant renommages
barras
2006-09-26
*
Declarative Proof Language: main commit
corbinea
2006-09-20
*
Standardisation du nom des méthodes de Evd
herbelin
2006-04-28
*
replacing whd_betaiotaevar_preserving_vm_cast
jforest
2006-04-14
*
Correction bug #842 (rename d'une hyp du contexte)
herbelin
2006-03-01
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
changement d'egalite pour le named_context_val
gregoire
2005-12-05
*
Changement des named_context
gregoire
2005-12-02
*
Confusion assert/error détectée par nouveau warning X de ocaml 3.09
herbelin
2005-11-04
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Protection against saving a proof with still non-instantiated evars (cf bug #...
herbelin
2005-04-29
*
Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...
herbelin
2004-12-31
*
Mise en page
herbelin
2004-11-17
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
deplacement de clenv vers pretyping
barras
2004-09-03
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tête
herbelin
2004-07-16
*
added breakpoints to help ide
corbinea
2004-02-26
*
Bug affichage des metas dans un environnement avec definitions locales (bug 277)
herbelin
2003-12-19
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
2 espaces en trop
herbelin
2003-11-05
*
Amelioration de l'afficheur de script structure
herbelin
2003-11-05
*
Paramétrisation vis à vis de existential_key
herbelin
2003-09-06
*
Ground update
corbinea
2003-07-08
*
Ground Update.
corbinea
2003-06-20
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
Affichage des tactiques en v8
herbelin
2003-04-07
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
Ajout d'un message à FailTac
herbelin
2003-03-31
*
simplification de solve_subgoal: n'utilise plus frontier
barras
2002-12-19
*
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
*
Intégration des modifs de la branche mowgli :
herbelin
2002-11-05
*
Protection contre l'encapsulage de FailError dans Exc_located (sinon, par exe...
herbelin
2002-07-11
*
Réorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
prterm -> prterm_env
filliatr
2002-02-08
*
compat ocaml 3.03
filliatr
2001-12-13
*
suppression de l'affichage des noeuds Change_evars
barras
2001-12-11
*
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
*
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
*
Problème d'affichage d'un . pour les Local_constraints; remplacement par Idtac
herbelin
2001-09-21
*
exceptions
barras
2001-09-14
*
Suppression de l'affichage du non-reparsable 'Local constraint change'
herbelin
2001-07-24
*
amelioration des messages d'erreurs vis a vis des evars
barras
2001-05-23
[next]