aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.ml
AgeCommit message (Expand)Author
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-06-13Fixed bug #2314 (inversion using not checking the correctness of its argumentsherbelin
2010-06-09Fix bug #2317: setoid_rewrite ignored binding lists. Slightlymsozeau
2010-05-10Removed an evar_merge in clenv_fchain which not only is incorrect butherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2004-09-03deplacement de clenv vers pretypingbarras
2004-09-03premiere reorganisation de l\'unificationbarras
2004-07-16Nouvelle en-têteherbelin
2004-07-13bugs #667 and #783 (mimick_evar and loc_table on large files)barras
2004-04-20Amélioration message d'erreur quand échec unificationclrenard
2003-11-15Amelioration du message d'erreur en cas de tentative d'instanciationclrenard
2003-10-10Suppression clenv_change_head que seul Wcclausenv utisaitherbelin
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
2003-03-28Réparation bug de l'unification. En effet, avant l'instanciation d'une evarclrenard
2002-12-30Amélioration choix des noms dans abstract_list_allherbelin
2002-12-24code mortherbelin
2002-12-23Tentative d'interdire les K-abstractions si allow_K est faux et leherbelin
2002-12-22Cas motif universelherbelin
2002-12-21Légère amélioration des messages d'erreur des with-bindings et des Rewriteherbelin
2002-12-20Prise en compte des coercions dans les 'with' bindingsherbelin
2002-12-19suite du commit precedentbarras
2002-12-13Compensation de suppression betaiota de type_of (suite)herbelin
2002-12-12Compensation de suppression betaiota de type_of (suite)herbelin
2002-12-11Compensation de suppression betaiota de type_ofherbelin
2002-10-09retour en arriere concernant la recherche d'occurence modulo expansion des le...barras
2002-10-01Vraie substitutivite de autohintscoq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-14modification de clenv_merge:barras
2002-04-17typed unification in the case of Patternbarras
2002-04-12backtrack unificationbarras
2002-04-12Re-introduction de clenv_constrain_missing_arg utilisé par la contrib Lannionherbelin
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
2002-04-10backtrack dans l'algo d'unificationbarras
2002-04-04resolution du pb d'efficacite du a Sign.add_named_declbarras
2002-04-03transformation des evar en meta preserve la linearite des metasbarras
2002-04-02- modifs de la condition de garde pour mieux tenir compte des raisonnementsbarras
2002-03-21backtrack de l'unificationbarras
2002-03-20encore quelques petites modif de l'unificationbarras
2002-03-12Propagation du pb de conversion dans clenv_unifyherbelin
2002-03-08renommage de fonctionsbarras
2002-03-05unification faite de gauche a droite (et non pas l'inverse) pour eviter quebarras
2002-03-04*** empty log message ***barras
2002-03-04Nouveau Rewrite-in plus economiquebarras
2002-02-28Generalisation de l'utilisation de l'unification d'ordre 2barras
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2002-02-12petite modif pour ne pas expanser trop de let pendant l'unificationbarras
2001-12-17Mauvais nom d'erreur d'échec de nthherbelin
2001-12-13compat ocaml 3.03filliatr
2001-11-29nouvel algo de conversion plus uniformebarras
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 15:46:45 +0000