aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mli
Commit message (Expand)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)Gravatar Enrico Tassi2018-02-19
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | [api] Remove aliases of `Evar.t`Gravatar Emilio Jesus Gallego Arias2017-11-26
| * Fix interpretation of global universes in univdecl constraints.Gravatar Gaëtan Gilbert2017-11-25
|/
* [api] A few more minor deprecation notices.Gravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* Remove understand_tcc_evars.Gravatar Maxime Dénès2017-08-01
* Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
* Remove understand_judgment and understand_judgment_tcc.Gravatar Maxime Dénès2017-08-01
* Remove allow_anonymous_refs.Gravatar Maxime Dénès2017-08-01
* Remove pure_open_constr (now open_constr)Gravatar Maxime Dénès2017-08-01
* Move glob_constr_ltac_closure to evar_refiner.Gravatar Maxime Dénès2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
| * Generalizing the tactic-in-term embedding to any generic argument.Gravatar Pierre-Marie Pédrot2017-05-03
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
| * Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Fix bug #4723 and FIXME in API for solve_by_tacGravatar Matthieu Sozeau2016-09-28
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Allow `Pretyping.search_guard` to not check guardGravatar Arnaud Spiwack2016-06-15
* | Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* | Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* | Making Evarutil independent from Reductionops.Gravatar Pierre-Marie Pédrot2016-03-20
* | Adding location to universes generated by the pretyper.Gravatar Pierre-Marie Pédrot2016-02-19
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\ \
| * | Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | | Using dynamic values in tactic evaluation.Gravatar Pierre-Marie Pédrot2015-12-21
* | | Removing dynamic inclusion of constrs in tactic AST.Gravatar Pierre-Marie Pédrot2015-12-04
|/ /
* | Documenting a bit more interpretation functions in passing.Gravatar Hugo Herbelin2015-10-26
* | Fixing #4221 (interpreting bound variables using ltac env was possiblyGravatar Hugo Herbelin2015-08-02
|/
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23