aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* Update headers.Gravatar Maxime Dénès2015-01-12
* Cleaning and documenting Clenv.make_evar_clauseGravatar Pierre-Marie Pédrot2014-10-27
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Lazily check that an argument is dependent when constructing evar clauses.Gravatar Pierre-Marie Pédrot2014-10-21
* Adding an evar version of the make_clenv function.Gravatar Pierre-Marie Pédrot2014-10-21
* Be more conservative and keep the use of eq_constr in pretyping/ functions.Gravatar Matthieu Sozeau2014-09-17
* Fix bug #3593, making constr_eq and progress work up toGravatar Matthieu Sozeau2014-09-17
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Referring to evars by names. Added a parser for evars (but parsing ofGravatar Hugo Herbelin2014-09-12
* A step towards better differentiating when w_unify is used for subtermGravatar Hugo Herbelin2014-09-10
* Fix set_leq_sort refusing max(u,Set) <= Set when u is flexible.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* 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