aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
Commit message (Expand)AuthorAge
* Removing some return type compatibility layers in Termops.Gravatar 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
* Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacticals 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
* Cases 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
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
* Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* Reordering Termops w.r.t. Evd and Namegen in engine folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
* | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | CLEANUP: removing "Termops.compact_named_context_reverse" functionGravatar Matej Kosik2016-08-26
* | CLEANUP: renaming "Context.ListNamed" module to "Context.Compacted"Gravatar Matej Kosik2016-08-26
* | CLEANUP: changing the definition of the "Context.NamedList.Declaration" typeGravatar Matej Kosik2016-08-25
* | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
* Moving extended_rel_vect/extended_rel_list to the kernel.Gravatar Hugo Herbelin2015-12-05
* About building of substitutions from instances.Gravatar Hugo Herbelin2015-12-05
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-26
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 06:23:33 +0000