aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
...
* | 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
* | Removing compatibility layers in RetypingGravatar 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
* | Tactic_matching API using EConstr.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
* | 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
* | Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Nativenorm 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-11-18
|/|
| * More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
* | Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\ \
| | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| |/
| * Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
| |\
| | * A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Gravatar Hugo Herbelin2016-10-20
* | | 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
* | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \
| * | | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ | | |/ / | |/| |
| * | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
| |\ \ \ | | | |/ | | |/|
| | * | Fixing #5077 (failure on typing a fixpoint with evars in its type).Gravatar Hugo Herbelin2016-09-10
| | | * Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
| |_|/ |/| |
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* | | | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | CLEANUP: taking advantage of "_ % _" operator to express function composition...Gravatar Matej Kosik2016-08-29
* | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\ \ \ \ | | |/ / | |/| |
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| * | | Do not recompute the whole evar naming environment in GProd intepretation.Gravatar Pierre-Marie Pédrot2016-08-21
| * | | Short path for Pretyping.ltac_interp_name_env.Gravatar Pierre-Marie Pédrot2016-08-21
|/ / /
| * | 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
| * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | Using a dedicated kind of substitutions in evar name generation.Gravatar Pierre-Marie Pédrot2016-08-06
* | Using the extended contexts in pretyping.Gravatar Pierre-Marie Pédrot2016-08-05
* | Embedding the pretyping environment in a dummy record.Gravatar Pierre-Marie Pédrot2016-08-04
* | Univs: fix internalization of (x := T) and castsGravatar Matthieu Sozeau2016-07-06
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 18:00:03 +0000