aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/tacred.ml
Commit message (Expand)AuthorAge
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cbv 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
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * 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
|/
* closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* 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
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Using monotonic types for conversion functions.Gravatar Pierre-Marie Pédrot2016-02-15
* | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
|/
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Fix 'don't expose cases' in cbnGravatar Pierre Boutillier2015-02-15
* Fixing bug #3490.Gravatar Pierre-Marie Pédrot2015-02-15
* Fixing bug #3916.Gravatar Pierre-Marie Pédrot2015-02-15
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Avoiding introducing yet another convention in naming files.Gravatar Hugo Herbelin2015-01-08
* Fixing detection of occurrences in the presence of nested subterms forGravatar Hugo Herbelin2014-11-18
* Cosmetic changes.Gravatar Hugo Herbelin2014-11-02
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Change reduction_of_red_expr to return an e_reduction_function returningGravatar Matthieu Sozeau2014-10-24
* Fix bug 3637.Gravatar Matthieu Sozeau2014-10-15
* Fix bug due to shadowing a variable name in tacredGravatar Matthieu Sozeau2014-10-10
* Fix semantics of matching with folded/unfolded projections to definitelyGravatar Matthieu Sozeau2014-09-27
* Fix bug 3662 by actually reducing primitive projections in cbv/compute.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Fix bug #3656.Gravatar Matthieu Sozeau2014-09-23
* Move the specific map_constr_with_binders_left_to_rightGravatar Matthieu Sozeau2014-09-19
* Fixing #3641 (loop in e_contextually, introduced in r16525).Gravatar Hugo Herbelin2014-09-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 10:58:14 +0000