aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* Do not generate useless argument arrays in whd_* functions.Gravatar ppedrot2013-10-29
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Removing useless evar-related stuff.Gravatar ppedrot2013-09-25
* Backtrack on unneeded change of interface for pose_metas_as_evars.Gravatar msozeau2013-06-04
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
* Removing a redundant function from Evd.Gravatar ppedrot2013-05-03
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Monomorphization (proof)Gravatar ppedrot2012-11-25
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Reductionops refactoringGravatar pboutill2012-07-20
* 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