aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fixing alpha-conversion bug #2723 introduced in r12485-12486.Gravatar herbelin2012-03-20
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Added a flag to restrict conversion in tactic unification on theGravatar herbelin2011-06-13
* Moved allow_K to a unification flagGravatar herbelin2011-06-10
* First phase removing obsolete support for eta up to conversion inGravatar herbelin2011-05-04
* Forgot a use of evars_reset_evd in nf_evars, add an optional argument asGravatar msozeau2011-03-10
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* Try to fix the behavior of clenv_missing used when declaring hintsGravatar letouzey2011-02-22
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Clenv.connect_clenv without its Evd.foldGravatar letouzey2010-12-15
* Delayed the evar normalization in error messages to the last minuteGravatar herbelin2010-11-07
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* In the computation of missing arguments for apply, accept that theGravatar herbelin2010-09-17
* Fix [clenv_missing] to compute a better approximation of missingGravatar msozeau2010-08-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* Fixed bug #2314 (inversion using not checking the correctness of its argumentsGravatar herbelin2010-06-13
* Fix bug #2317: setoid_rewrite ignored binding lists. SlightlyGravatar msozeau2010-06-09
* Removed an evar_merge in clenv_fchain which not only is incorrect butGravatar herbelin2010-05-10
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* deplacement de clenv vers pretypingGravatar barras2004-09-03
* premiere reorganisation de l\'unificationGravatar barras2004-09-03
* Nouvelle en-têteGravatar herbelin2004-07-16
* bugs #667 and #783 (mimick_evar and loc_table on large files)Gravatar barras2004-07-13
* Amélioration message d'erreur quand échec unificationGravatar clrenard2004-04-20
* Amelioration du message d'erreur en cas de tentative d'instanciationGravatar clrenard2003-11-15
* Suppression clenv_change_head que seul Wcclausenv utisaitGravatar herbelin2003-10-10
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* Réparation bug de l'unification. En effet, avant l'instanciation d'une evarGravatar clrenard2003-03-28
* Amélioration choix des noms dans abstract_list_allGravatar herbelin2002-12-30
* code mortGravatar herbelin2002-12-24
* Tentative d'interdire les K-abstractions si allow_K est faux et leGravatar herbelin2002-12-23
* Cas motif universelGravatar herbelin2002-12-22
* Légère amélioration des messages d'erreur des with-bindings et des RewriteGravatar herbelin2002-12-21
* Prise en compte des coercions dans les 'with' bindingsGravatar herbelin2002-12-20
* suite du commit precedentGravatar barras2002-12-19
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-13
* Compensation de suppression betaiota de type_of (suite)Gravatar herbelin2002-12-12
* Compensation de suppression betaiota de type_ofGravatar herbelin2002-12-11
* retour en arriere concernant la recherche d'occurence modulo expansion des le...Gravatar barras2002-10-09
* Vraie substitutivite de autohintsGravatar coq2002-10-01
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29