index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
interp
/
constrintern.mli
Age
Commit message (
Expand
)
Author
2007-05-06
Nouveaux changements autour des implicites (notamment suite à
herbelin
2007-04-29
Multiples changements autour des implicites :
herbelin
2007-03-28
Support for implicit formal argument types in Program ; parse types in type s...
msozeau
2007-02-13
Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de
herbelin
2006-09-20
Declarative Proof Language: main commit
corbinea
2006-09-01
Export de fonctions d'interprétation acceptant des evars non résolues
herbelin
2005-12-26
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-21
Restructuration des points d'entrée de Pretyping et Constrintern
herbelin
2005-09-09
Conséquences nettoyage pretyping.ml
herbelin
2005-01-21
Compatibilité ocamlweb pour cible doc
herbelin
2004-07-16
Nouvelle en-tête
herbelin
2004-04-17
pb facto des Fixpoint + erreur avec -dump-glob et Load
barras
2004-03-27
Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...
herbelin
2003-11-24
Prise en compte des defs syntaxiques dans is_global et global_reference qui p...
herbelin
2003-10-14
Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...
herbelin
2003-10-08
Prise en compte des paramètres implicites d'inductifs pour la globalisation ...
herbelin
2003-09-06
cosmetique
herbelin
2003-05-21
Suppression définitive de lmatch et or_metanum dans tacinterp
herbelin
2003-05-19
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
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-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-02
Re-déplacement du résultat de Grammar au niveau constr_expr
herbelin
2002-11-14
Réforme de l'interprétation des termes :
herbelin