aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/leminv.ml
Commit message (Expand)AuthorAge
* Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
* [econstr] Switch constrintern API to non-imperative style.Gravatar Emilio Jesus Gallego Arias2017-12-15
* Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
* Stop exposing UState.universe_context and its Evd wrapper.Gravatar Gaëtan Gilbert2017-11-24
* Separate checking univ_decls and obtaining universe binder names.Gravatar Gaëtan Gilbert2017-11-24
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Removing compatibility layer in Leminv.Gravatar Pierre-Marie Pédrot2017-04-24
* 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
* Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Clenv 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 branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Stylistic improvements in intf/decl_kinds.mli.Gravatar Maxime Dénès2016-09-20
| * Tracking careless uses of slow name lookup.Gravatar Pierre-Marie Pédrot2016-09-09
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \
* | | 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
|/
* 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
* 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
* | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Univs: local names handling.Gravatar Matthieu Sozeau2015-10-28
* | Boxing the Goal.enter primitive into a record type.Gravatar Pierre-Marie Pédrot2015-10-20
|/
* Fix some typos.Gravatar Guillaume Melquiond2015-10-13
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Fix bug #2775: Correct handling of universes in leminv.Gravatar Matthieu Sozeau2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* 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
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06