index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrintern.ml
Age
Commit message (
Expand
)
Author
2003-09-18
Parsing correct des explicites en cas de projection
herbelin
2003-09-12
Scope type pour le codomaine de Prod aussi
herbelin
2003-09-09
Ajout If; synchro avec constrextern
herbelin
2003-09-06
cosmetique
herbelin
2003-09-02
Plus de passage du scope tmp sous les lambdas
herbelin
2003-08-31
Symetrisation des changements implicites de scope
herbelin
2003-08-11
Nouvelle mouture du traducteur v7->v8
herbelin
2003-06-10
Ajout notation c.(f) en v8 pour les projections de Record
herbelin
2003-05-21
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-21
Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ...
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
herbelin
2003-05-14
Hack pour ameliorer l'affichage des applications dans les `...` et
herbelin
2003-04-10
Affichage forcé des implicites contextuels si pas de contexte connu
herbelin
2003-04-09
Mécanisme plus simple et efficace pour traduire les implicites
herbelin
2003-04-07
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-03-29
Implicit Variables Type dans les inductive
herbelin
2003-03-29
Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)
herbelin
2003-03-12
*** empty log message ***
barras
2003-01-19
Erreur sur precedent commit
herbelin
2003-01-19
Restructuration interpréteur de tactique: plus d'évaluation partielle à la...
herbelin
2002-12-15
Prise en compte des scopes traversés dans les notations
herbelin
2002-12-03
Préparation à la prise en compte des changements de scopes internes aux not...
herbelin
2002-12-02
Re-déplacement du résultat de Grammar au niveau constr_expr
herbelin
2002-11-26
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-24
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-15
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-14
Réforme de l'interprétation des termes :
herbelin
[prev]