From b14d88c8cd17ad524898b31c1772a0e8f70f19f8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 16 May 2015 12:33:32 +0200
Subject: Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".

---
 tactics/tactics.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2791d7c484..402a9e88a1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3597,8 +3597,11 @@ let find_induction_type isrec elim hyp0 gl =
 	if Option.is_empty scheme.indarg then error "Cannot find induction type";
 	let indsign = compute_scheme_signature scheme hyp0 ind_guess in
 	let elim = ({elimindex = Some(-1); elimbody = elimc; elimrename = None},elimt) in
-	scheme, ElimUsing (elim,indsign) in
-  (Option.get scheme.indref,scheme.nparams, elim)
+	scheme, ElimUsing (elim,indsign)
+  in
+  match scheme.indref with
+  | None -> error_ind_scheme ""
+  | Some ref -> ref, scheme.nparams, elim
 
 let get_elim_signature elim hyp0 gl =
   compute_elim_signature (given_elim hyp0 elim gl) hyp0
-- 
cgit v1.2.3