diff options
| author | Hugo Herbelin | 2018-09-28 18:40:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-28 18:51:02 +0200 |
| commit | 2ea68be1bf7b5977234957f8ad04fdaa0ce539a2 (patch) | |
| tree | e798ed949c909b949ae04b4fc29e59653a119077 /tactics | |
| parent | 0bcbc990dcebce2e66f10aba462c9fed2c2eda06 (diff) | |
Functionalizing calls to the environment in Himsg.
This shall eventually allow to call Himsg at any point of the
execution, independently of the exact current global environment.
Diffstat (limited to 'tactics')
| -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 43786c8e19..f718b13a63 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -495,7 +495,7 @@ let raw_inversion inv_kind id status names = (* Error messages of the inversion tactics *) let wrap_inv_error id = function (e, info) -> match e with | Indrec.RecursionSchemeError - (Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> + (_, Indrec.NotAllowedCaseAnalysis (_,(Type _ | Set as k),i)) -> Proofview.tclENV >>= fun env -> Proofview.tclEVARMAP >>= fun sigma -> tclZEROMSG ( |