diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-22 19:45:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-26 15:34:50 +0200 |
| commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
| tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /tactics/inv.ml | |
| parent | 925c434592597a34cd7ef4efb5e18a43e197bd96 (diff) | |
Passing around the flag for injection so that tactics calling inj at
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index f391382bf..c5aa74ba5 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -371,7 +371,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = (* If no immediate variable in the equation, try to decompose it *) (* and apply a trailer which again try to substitute *) (fun id -> - dEqThen false (deq_trailer id) + dEqThen ~keep_proofs:None false (deq_trailer id) (Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings)))) id |