aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/pfedit.ml
Commit message (Expand)AuthorAge
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* Proof engine: support for nesting tactic-in-term within other tactics.Gravatar Hugo Herbelin2018-03-08
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Fix #6323: stronger restrict universe context vs abstract.Gravatar Gaëtan Gilbert2017-12-06
* Cleanup API for registering universe binders.Gravatar Matthieu Sozeau2017-12-01
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Remove 8.7 ML-deprecated functions.Gravatar Emilio Jesus Gallego Arias2017-11-07
* [stm] Remove state-handling from Futures.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
* Statically ensuring that inlined entries out of the kernel have no effects.Gravatar Pierre-Marie Pédrot2017-07-26
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* Don't double up on periods in anomaliesGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| |/
| * Remove a dead exception catching code.Gravatar Théo Zimmermann2017-03-13
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\|
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv 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
| * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
* | 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
* | 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
* | 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
|/
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
| * Fixing #4881 (synchronizing "Declare Implicit Tactic" with backtrack).Gravatar Hugo Herbelin2016-07-01
| * Fixing #4882 (anomaly with Declare Implicit Tactic on hole of type with evars).Gravatar Hugo Herbelin2016-07-01
* | Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-01
|\|
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| * Pfedit.get_current_context refinement (fix #4523)Gravatar Matthieu Sozeau2016-05-26
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\|
| * Univs: fix get_current_context (bug #4603, part I)Gravatar Matthieu Sozeau2016-03-25
* | Moving VernacSolve to an EXTEND-based definition.Gravatar Pierre-Marie Pédrot2016-03-19
* | Removing the dependency in VernacSolve in the STM.Gravatar Pierre-Marie Pédrot2016-03-19
* | 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-11-29
|\|