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
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
* | 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-12 22:00:17 +0000