From 3ff3c18031317dcd08bf081e55212617b8820647 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Apr 2020 16:21:33 +0200
Subject: Return an option in lookup_scheme.

---
 plugins/ltac/rewrite.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f002bbc57a..3834b21a14 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -952,10 +952,11 @@ let fold_match env sigma c =
         then case_dep_scheme_kind_from_type
         else case_scheme_kind_from_type)
     in
-    let exists = Ind_tables.check_scheme sk ci.ci_ind in
-      if exists then
-        dep, pred, exists, Ind_tables.lookup_scheme sk ci.ci_ind
-      else raise Not_found
+    match Ind_tables.lookup_scheme sk ci.ci_ind with
+    | Some cst ->
+        dep, pred, true, cst
+    | None ->
+      raise Not_found
   in
   let app =
     let ind, args = Inductiveops.find_mrectype env sigma cty in
-- 
cgit v1.2.3