aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.mli
AgeCommit message (Expand)Author
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Multiples changements autour des implicites :herbelin
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-02-13Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé deherbelin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-09-01Export de fonctions d'interprétation acceptant des evars non résoluesherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-12-21Restructuration des points d'entrée de Pretyping et Constrinternherbelin
2005-09-09Conséquences nettoyage pretyping.mlherbelin
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-07-16Nouvelle en-têteherbelin
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
2004-03-27Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...herbelin
2003-11-24Prise en compte des defs syntaxiques dans is_global et global_reference qui p...herbelin
2003-10-14Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entre...herbelin
2003-10-08Prise en compte des paramètres implicites d'inductifs pour la globalisation ...herbelin
2003-09-06cosmetiqueherbelin
2003-05-21Suppression définitive de lmatch et or_metanum dans tacinterpherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-04-09Mécanisme plus simple et efficace pour traduire les implicitesherbelin
2003-04-07Globalisation des noms de tactiques dans les définitions de tactiquesherbelin
2003-03-29Implicit Variables Type dans les inductiveherbelin
2003-01-19Restructuration interpréteur de tactique: plus d'évaluation partielle à la...herbelin
2002-12-15Prise en compte des scopes traversés dans les notationsherbelin
2002-12-02Re-déplacement du résultat de Grammar au niveau constr_exprherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin