aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
...
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases 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
* | Retyping 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
| * Fixing injection in the presence of let-in in constructors.Gravatar Hugo Herbelin2016-12-22
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * fixing bug 4609: document an option governing the generation of equalitiesGravatar Yves Bertot2016-10-03
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-02
| |\
| | * Quick fix to another bug of "subst" introduced in 4e3d464 and spotted by Maxime.Gravatar Hugo Herbelin2016-09-30
| * | Merge branch 'v8.5' into v8.6Gravatar Maxime Dénès2016-09-30
| |\|
| | * Fix a bug in subst releaved by an OCaml warning.Gravatar Maxime Dénès2016-09-29
* | | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionGravatar Matej Kosik2016-08-25
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
| |/ / |/| |
* | | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-21
|\ \ \ | | |/ | |/|
| * | Remove extraneous dot in error message (bug #4832).Gravatar Guillaume Melquiond2016-08-19
| | * 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
| |/ |/|
* | Fixing #3070 ("subst" taking properly into account chains of dependencies).Gravatar Hugo Herbelin2016-08-17
* | Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
* | Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* | Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* | Removing the old refine tactic from the Tactics module.Gravatar Pierre-Marie Pédrot2016-05-17
* | Put the "exact" family of tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | Put the "clear" tactic into the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * In Regular Subst Tactic mode, ensure that the order of hypotheses isGravatar Hugo Herbelin2016-05-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-09
|\|
| * Fix strategy of Keyed UnificationGravatar Matthieu Sozeau2016-03-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\|
* | Exporting build_selector, a component of discriminate, for use in congruence.Gravatar Hugo Herbelin2016-03-05
| * Fix bug #4544: Backtrack on using full betaiota reduction during keyed unific...Gravatar Matthieu Sozeau2016-02-23
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Code factorization of tactic "unfold_body".Gravatar Pierre-Marie Pédrot2016-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 13:05:05 +0000