aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
AgeCommit message (Expand)Author
2018-01-17Use let-in aware prod_applist_assum in dtauto and firstorder.Jasper Hugunin
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-05Cosmetic changes in evar_map printer.Hugo Herbelin
2017-11-05Preventively protect locally against failures of evar_map printer.Hugo Herbelin
2017-09-28Efficient computation of the names contained in an environment.Pierre-Marie Pédrot
2017-09-12Port is_Set and is_Type to EConstr, as was is_Prop already.Guillaume Melquiond
2017-08-01Merge PR #913: Less allocations in DetypingMaxime Dénès
2017-07-26Removing template polymorphism for definitions.Pierre-Marie Pédrot
2017-07-21No useless reallocation in Termops.collapse_appl.Pierre-Marie Pédrot
2017-07-13Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Squashed commit of the following:Amin Timany
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-01Using delayed universe instances in EConstr.Pierre-Marie Pédrot
2017-04-01Actually exporting delayed universes in the EConstr implementation.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-14Removing some return type compatibility layers in Termops.Pierre-Marie Pédrot
2017-02-14Reductionops now return EConstrs.Pierre-Marie Pédrot
2017-02-14Eliminating parts of the right-hand side compatibility layerPierre-Marie Pédrot
2017-02-14Rewrite API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2017-02-14Leminv API using EConstr.Pierre-Marie Pédrot
2017-02-14Inv API using EConstr.Pierre-Marie Pédrot
2017-02-14Equality API using EConstr.Pierre-Marie Pédrot
2017-02-14Tactics API using EConstr.Pierre-Marie Pédrot
2017-02-14Hipattern API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacticals API using EConstr.Pierre-Marie Pédrot
2017-02-14Making judgment type generic over the type of inner constrs.Pierre-Marie Pédrot
2017-02-14Unification API using EConstr.Pierre-Marie Pédrot
2017-02-14Cases API using EConstr.Pierre-Marie Pédrot
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2017-02-14Tacred API using EConstr.Pierre-Marie Pédrot
2017-02-14Evarconv API using EConstr.Pierre-Marie Pédrot
2017-02-14Termops API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 14:03:30 +0000