aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/clenv.ml
Commit message (Expand)AuthorAge
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* Optim in Clenv: use noccurn instead of depends.Gravatar Pierre-Marie Pédrot2016-06-24
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\
| * Another fix to #4782 (a typing error not captured when dealing with bindings).Gravatar Hugo Herbelin2016-06-12
| * Fixing #4782 (a typing error not captured when dealing with bindings).Gravatar Hugo Herbelin2016-06-11
* | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 16:12:27 +0000