aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|
* | Inlining the only use of Clenv.connect_clenv.Gravatar Pierre-Marie Pédrot2015-11-18
| * Performance fix for destruct.Gravatar Pierre-Marie Pédrot2015-11-17
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* | Removing meta_with_name from Evd.Gravatar Pierre-Marie Pédrot2015-09-27
* | Removing uselessly duplicated function in Evd.Gravatar Pierre-Marie Pédrot2015-09-27
|/
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* 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