aboutsummaryrefslogtreecommitdiff
path: root/proofs/clenv.ml
AgeCommit message (Expand)Author
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2012-03-14Second step of integration of Program:msozeau
2012-03-02Noise for nothingpboutill
2011-10-11Moved to a more standard order of arguments (i.e. env followed by evar_map)herbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-05-04First phase removing obsolete support for eta up to conversion inherbelin
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-02-22Try to fix the behavior of clenv_missing used when declaring hintsletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-15Clenv.connect_clenv without its Evd.foldletouzey
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-17In the computation of missing arguments for apply, accept that theherbelin
2010-08-02Fix [clenv_missing] to compute a better approximation of missingmsozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-21 13:17:21 +0000