index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
refiner.mli
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
*
Messages de idtac et fail peuvent maintenant être des listes de string, int ...
herbelin
2006-01-21
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...
herbelin
2004-12-31
*
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
*
Nouvelle en-tête
herbelin
2004-07-16
*
Idtac peut prendre un argument à afficher
narboux
2003-11-12
*
Amelioration de l'afficheur de script structure
herbelin
2003-11-05
*
Ground Update.
corbinea
2003-06-20
*
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-19
*
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éorganisation des tclTHEN (cf dev/changements.txt)
herbelin
2002-05-29
*
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
Erreur dans un commentaire ...
clrenard
2001-05-18
*
entetes
filliatr
2001-03-15
*
application patch Cuit Alvarado : tclTHENSi et intros_until_n exportés
filliatr
2001-02-01
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Simplifications autour de typed_type (renommé types par analogie avec sorts)...
herbelin
2000-10-18
*
Renommage canonique :
herbelin
2000-10-18
*
Code redondant
herbelin
2000-10-13
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Modifs d'interpretation de patterns
delahaye
2000-07-21
*
Doc
herbelin
2000-05-23
*
Retrait du i pour tclTHEN_i et correction bugs Decompose
herbelin
2000-05-16
*
Nettoyage de l'interface de Pfedit
herbelin
2000-05-04
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
modifs pour premiere edition de liens
filliatr
1999-12-02
*
module Pfedit
filliatr
1999-12-01
*
- documentation repertoire proofs/
filliatr
1999-10-20
*
module Refiner
filliatr
1999-10-19
*
les variables existentielles contiennent maintenant un environnement (type
filliatr
1999-10-19
*
- déplacement (encore une fois !) des variables existentielles : elles sont
filliatr
1999-10-18