From 90871c4e9b2c2ea6983f4f37e33dd9c6fd2854a7 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Fri, 16 Apr 2021 06:24:17 +0200
Subject: Catch UserError in Hipattern.match_with_equation in case name is not
 yet registered

---
 tactics/hipattern.ml | 53 +++++++++++++++++++++++++++-------------------------
 1 file changed, 28 insertions(+), 25 deletions(-)

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 5338e0eef5..783a317b3a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -293,31 +293,34 @@ let match_with_equation env sigma t =
   let (hdapp,args) = destApp sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind,u) ->
-    if Coqlib.check_ind_ref "core.eq.type" ind then
-      Some (build_coq_eq_data()),hdapp,
-      PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-    else if Coqlib.check_ind_ref "core.identity.type" ind then
-      Some (build_coq_identity_data()),hdapp,
-      PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-    else if Coqlib.check_ind_ref "core.JMeq.type" ind then
-      Some (build_coq_jmeq_data()),hdapp,
-      HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
-    else
-      let (mib,mip) = Global.lookup_inductive ind in
-        let constr_types = mip.mind_nf_lc in
-        let nconstr = Array.length mip.mind_consnames in
-        if Int.equal nconstr 1 then
-          let (ctx, cty) = constr_types.(0) in
-          let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
-          if is_matching env sigma coq_refl_leibniz1_pattern cty then
-            None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
-          else if is_matching env sigma coq_refl_leibniz2_pattern cty then
-            None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
-          else if is_matching env sigma coq_refl_jm_pattern cty then
-            None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
-          else raise NoEquationFound
-        else raise NoEquationFound
-    | _ -> raise NoEquationFound
+    (try
+       if Coqlib.check_ind_ref "core.eq.type" ind then
+         Some (build_coq_eq_data()),hdapp,
+         PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+       else if Coqlib.check_ind_ref "core.identity.type" ind then
+         Some (build_coq_identity_data()),hdapp,
+         PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+       else if Coqlib.check_ind_ref "core.JMeq.type" ind then
+         Some (build_coq_jmeq_data()),hdapp,
+         HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+       else
+         let (mib,mip) = Global.lookup_inductive ind in
+         let constr_types = mip.mind_nf_lc in
+         let nconstr = Array.length mip.mind_consnames in
+         if Int.equal nconstr 1 then
+           let (ctx, cty) = constr_types.(0) in
+           let cty = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
+           if is_matching env sigma coq_refl_leibniz1_pattern cty then
+             None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1))
+           else if is_matching env sigma coq_refl_leibniz2_pattern cty then
+             None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2))
+           else if is_matching env sigma coq_refl_jm_pattern cty then
+             None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3))
+           else raise NoEquationFound
+         else raise NoEquationFound
+     with UserError _ ->
+       raise NoEquationFound)
+  | _ -> raise NoEquationFound
 
 (* Note: An "equality type" is any type with a single argument-free
    constructor: it captures eq, eq_dep, JMeq, eq_true, etc. but also
-- 
cgit v1.2.3