aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* 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
* | | Moving conversion functions to the new tactic API.Gravatar Pierre-Marie Pédrot2016-02-15
| * | 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
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | | Fixing an "injection as" bug in the presence of side conditions.Gravatar Hugo Herbelin2015-12-25
|/ /
* | Granting clear_flag in injection, even legacy mode. This is possibleGravatar Hugo Herbelin2015-12-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-20
|\|