From 2ea68be1bf7b5977234957f8ad04fdaa0ce539a2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Sep 2018 18:40:10 +0200
Subject: 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.
---
 tactics/inv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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 (
-- 
cgit v1.2.3