Merge PR #10635: [funind] Port indfun to the new tactic engine.

Reviewed-by: ppedrot

8 files changed, 213 insertions, 195 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 5a939b4adf..ca33e4e757 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -941,7 +941,11 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
 let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
   let equation_lemma =
     try
-      let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in
+      let finfos =
+        match find_Function_infos (fst (destConst !evd f)) (*FIXME*) with
+        | None -> raise Not_found
+        | Some finfos -> finfos
+      in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
       let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in
@@ -953,14 +957,18 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
       let _ =
         match e with
           | Option.IsNone ->
-              let finfos = find_Function_infos (fst (destConst !evd f)) in
-              update_Function
-                {finfos with
-                   equation_lemma = Some (match Nametab.locate (qualid_of_ident equation_lemma_id) with
-                                              GlobRef.ConstRef c -> c
-                                            | _ -> CErrors.anomaly (Pp.str "Not a constant.")
-                                         )
-                }
+            let finfos = match find_Function_infos (fst (destConst !evd f)) with
+              | None -> raise Not_found
+              | Some finfos -> finfos
+            in
+            update_Function
+              {finfos with
+               equation_lemma = Some (
+                   match Nametab.locate (qualid_of_ident equation_lemma_id) with
+                   | GlobRef.ConstRef c -> c
+                   | _ -> CErrors.anomaly (Pp.str "Not a constant.")
+                 )
+              }
           | _ -> ()
       in
       (* let res = Constrintern.construct_reference (pf_hyps g) equation_lemma_id in *)
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index 92a93489f4..2b990400e3 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -91,7 +91,7 @@ END
 {
 
 let functional_induction b c x pat =
-  Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
+  functional_induction true c x (Option.map out_disjunctive pat)
 
 }
 
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a836335d4d..60717c6eec 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -495,14 +495,17 @@ let find_induction_principle evd f =
     | Constr.Const c' -> c'
     | _ -> CErrors.user_err Pp.(str "Must be used with a function")
   in
-  let infos = find_Function_infos f_as_constant in
-  match infos.rect_lemma with
-  | None -> raise Not_found
-  | Some rect_lemma ->
-    let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
-    let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
-    evd:=evd';
-    rect_lemma,typ
+  match find_Function_infos f_as_constant with
+  | None ->
+    raise Not_found
+  | Some infos ->
+    match infos.rect_lemma with
+    | None -> raise Not_found
+    | Some rect_lemma ->
+      let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (GlobRef.ConstRef rect_lemma) in
+      let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+      evd:=evd';
+      rect_lemma,typ
 
 (* [prove_fun_correct funs_constr graphs_constr schemes lemmas_types_infos i ]
    is the tactic used to prove correctness lemma.
@@ -1016,12 +1019,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tacti
     *)
     let rewrite_tac j ids : Tacmach.tactic =
       let graph_def = graphs.(j) in
-      let infos =
-        try find_Function_infos (fst (destConst (project g) funcs.(j)))
-        with Not_found -> CErrors.user_err Pp.(str "No graph found")
+      let infos = match find_Function_infos (fst (destConst (project g) funcs.(j))) with
+        | None ->
+          CErrors.user_err Pp.(str "No graph found")
+        | Some infos -> infos
       in
-      if infos.is_general
-      || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
+      if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.Declarations.mind_recargs
       then
         let eq_lemma =
           try Option.get (infos).equation_lemma
@@ -1174,9 +1177,9 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   let first_fun = List.hd funs in
   let funs_mp = KerName.modpath (Constant.canonical (fst first_fun)) in
   let first_fun_kn =
-    try
-      fst (find_Function_infos  (fst first_fun)).graph_ind
-    with Not_found -> raise No_graph_found
+    match find_Function_infos (fst first_fun) with
+    | None -> raise No_graph_found
+    | Some finfos -> fst finfos.graph_ind
   in
   let this_block_funs_indexes = get_funs_constant funs_mp (fst first_fun) in
   let this_block_funs = Array.map (fun (c,_) -> (c,snd first_fun)) this_block_funs_indexes in
@@ -1231,12 +1234,15 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
   in
   incr i;
   let opacity =
-    let finfos = find_Function_infos (fst first_fun) in
-    try
-      let equation =  Option.get finfos.equation_lemma in
+    let finfos =
+      match find_Function_infos (fst first_fun) with
+      | None -> raise Not_found
+      | Some finfos -> finfos
+    in
+    match finfos.equation_lemma with
+    | None -> false (* non recursive definition *)
+    | Some equation ->
       Declareops.is_opaque (Global.lookup_constant equation)
-    with Option.IsNone -> (* non recursive definition *)
-      false
   in
   let const = {const with Proof_global.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
@@ -1381,7 +1387,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
             let lemma = fst @@ Lemmas.by
                 (Proofview.V82.tactic (proving_tac i)) lemma in
             let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-            let finfo = find_Function_infos (fst f_as_constant) in
+            let finfo =
+              match find_Function_infos (fst f_as_constant) with
+              | None -> raise Not_found
+              | Some finfo -> finfo
+            in
             (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
             let _,lem_cst_constr = Evd.fresh_global
                 (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
@@ -1443,7 +1453,11 @@ let derive_correctness (funs: Constr.pconstant list) (graphs:inductive list) =
                                (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
                                                         (proving_tac i))) lemma) in
             let () = Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
-            let finfo = find_Function_infos (fst f_as_constant) in
+            let finfo =
+              match find_Function_infos (fst f_as_constant) with
+              | None -> raise Not_found
+              | Some finfo -> finfo
+            in
             let _,lem_cst_constr = Evd.fresh_global
                 (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
             let (lem_cst,_) = destConst !evd lem_cst_constr in
@@ -2028,7 +2042,11 @@ let build_case_scheme fa =
   let sigma, (_,u) = Evd.fresh_constant_instance env sigma funs in
   let first_fun = funs in
   let funs_mp = Constant.modpath first_fun in
-  let first_fun_kn = try fst (find_Function_infos  first_fun).graph_ind with Not_found -> raise No_graph_found in
+  let first_fun_kn =
+    match find_Function_infos first_fun with
+    | None -> raise No_graph_found
+    | Some finfos -> fst finfos.graph_ind
+  in
   let this_block_funs_indexes = get_funs_constant funs_mp first_fun in
   let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in
   let prop_sort = Sorts.InProp in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index eeb2f246c2..2937ae5d14 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,15 +8,19 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
-open Sorts
+open Pp
 open Util
+open CErrors
 open Names
+open Sorts
 open Constr
 open EConstr
-open Pp
+
+open Tacmach.New
+open Tacticals.New
+open Tactics
+
 open Indfun_common
-open Tactypes
 
 module RelDecl = Context.Rel.Declaration
 
@@ -37,111 +41,106 @@ let choose_dest_or_ind scheme_info args =
   Tactics.induction_destruct (is_rec_info sigma scheme_info) false args)
 
 let functional_induction with_clean c princl pat =
-  let res =
-    fun g ->
-    let sigma = Tacmach.project g in
+  let open Proofview.Notations in
+  Proofview.Goal.enter_one (fun gl ->
+    let sigma = project gl in
     let f,args = decompose_app sigma c in
-    let princ,bindings, princ_type,g' =
-      match princl with
-      | None -> (* No principle is given let's find the good one *)
-         begin
-           match EConstr.kind sigma f with
-           | Const (c',u) ->
-              let princ_option =
-                let finfo = (* we first try to find out a graph on f *)
-                  try find_Function_infos c'
-                  with Not_found ->
-                    user_err  (str "Cannot find induction information on "++
-                                       Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
-                in
-                match Tacticals.elimination_sort_of_goal g with
-                | InSProp -> finfo.sprop_lemma
-                | InProp -> finfo.prop_lemma
-                | InSet -> finfo.rec_lemma
-                | InType -> finfo.rect_lemma
+    match princl with
+    | None -> (* No principle is given let's find the good one *)
+      begin
+        match EConstr.kind sigma f with
+        | Const (c',u) ->
+          let princ_option =
+            let finfo = (* we first try to find out a graph on f *)
+              match find_Function_infos c' with
+              | Some finfo -> finfo
+              | None ->
+                user_err  (str "Cannot find induction information on "++
+                           Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
+            in
+            match elimination_sort_of_goal gl with
+            | InSProp -> finfo.sprop_lemma
+            | InProp -> finfo.prop_lemma
+            | InSet -> finfo.rec_lemma
+            | InType -> finfo.rect_lemma
+          in
+          let princ =  (* then we get the principle *)
+            match princ_option with
+            | Some princ ->
+              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) (GlobRef.ConstRef princ) in
+              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+              Proofview.tclUNIT princ
+            | None ->
+              (*i If there is not default lemma defined then,
+                      we cross our finger and try to find a lemma named f_ind
+                      (or f_rec, f_rect) i*)
+              let princ_name =
+                Indrec.make_elimination_ident
+                  (Label.to_id (Constant.label c'))
+                  (elimination_sort_of_goal gl)
               in
-              let princ,g' =  (* then we get the principle *)
+              let princ_ref =
                 try
-                  let g',princ =
-                    Tacmach.pf_eapply (Evd.fresh_global) g  (GlobRef.ConstRef (Option.get princ_option )) in
-                  princ,g'
-                with Option.IsNone ->
-                  (*i If there is not default lemma defined then,
-                          we cross our finger and try to find a lemma named f_ind
-                          (or f_rec, f_rect) i*)
-                  let princ_name =
-                    Indrec.make_elimination_ident
-                      (Label.to_id (Constant.label c'))
-                      (Tacticals.elimination_sort_of_goal g)
-                  in
-                  try
-                    let princ_ref = const_of_id princ_name in
-                    let (a,b) = Tacmach.pf_eapply (Evd.fresh_global) g princ_ref in
-                    (b,a)
-                    (* mkConst(const_of_id princ_name ),g (\* FIXME *\) *)
-                  with Not_found -> (* This one is neither defined ! *)
-                    user_err  (str "Cannot find induction principle for "
-                                     ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
+                  Constrintern.locate_reference (Libnames.qualid_of_ident princ_name)
+                with
+                | Not_found ->
+                  user_err (str "Cannot find induction principle for "
+                            ++ Printer.pr_leconstr_env (pf_env gl) sigma (mkConst c') )
               in
-              (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
-           | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
-         end
-      | Some ((princ,binding)) ->
-         princ,binding,Tacmach.pf_unsafe_type_of g princ,g
-    in
-    let sigma = Tacmach.project g' in
-    let princ_infos = Tactics.compute_elim_sig (Tacmach.project g') princ_type in
-    let args_as_induction_constr =
-      let c_list =
-        if princ_infos.Tactics.farg_in_concl
-        then [c] else []
-      in
-      if List.length args + List.length c_list = 0
-      then user_err Pp.(str "Cannot recognize a valid functional scheme" );
-      let encoded_pat_as_patlist =
-        List.make (List.length args + List.length c_list - 1) None @ [pat]
-      in
-      List.map2
-        (fun c pat ->
-          ((None,
-            Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
-           (None,pat),
-           None))
-        (args@c_list)
-        encoded_pat_as_patlist
-    in
-    let princ' = Some (princ,bindings) in
-    let princ_vars =
-      List.fold_right
-        (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
-        args
-        Id.Set.empty
+              let sigma, princ = Evd.fresh_global (pf_env gl) (project gl) princ_ref in
+              Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+              Proofview.tclUNIT princ
+          in
+          princ >>= fun princ ->
+          (* We need to refresh gl due to the updated evar_map in princ *)
+          Proofview.Goal.enter_one (fun gl ->
+          Proofview.tclUNIT (princ, Tactypes.NoBindings, pf_unsafe_type_of gl princ, args))
+        | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
+      end
+    | Some ((princ,binding)) ->
+      Proofview.tclUNIT (princ, binding, pf_unsafe_type_of gl princ, args)
+    ) >>= fun (princ, bindings, princ_type, args) ->
+  Proofview.Goal.enter (fun gl ->
+  let sigma = project gl in
+  let princ_infos = compute_elim_sig (project gl) princ_type in
+  let args_as_induction_constr =
+    let c_list =
+      if princ_infos.Tactics.farg_in_concl
+      then [c] else []
     in
-    let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in
-    let old_idl = Id.Set.diff old_idl princ_vars in
-    let subst_and_reduce g =
-      if with_clean
-      then
-        let idl =
-          List.filter (fun id -> not (Id.Set.mem id old_idl))
-            (Tacmach.pf_ids_of_hyps g)
-        in
-        let flag =
-          Genredexpr.Cbv
-            {Redops.all_flags
-             with Genredexpr.rDelta = false;
-            }
-        in
-        Tacticals.tclTHEN
-          (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
-          (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
-          g
-      else Tacticals.tclIDTAC g
+    if List.length args + List.length c_list = 0
+    then user_err Pp.(str "Cannot recognize a valid functional scheme" );
+    let encoded_pat_as_patlist =
+      List.make (List.length args + List.length c_list - 1) None @ [pat]
     in
-    Tacticals.tclTHEN
-      (Proofview.V82.of_tactic (choose_dest_or_ind
-         princ_infos
-         (args_as_induction_constr,princ')))
-      subst_and_reduce
-      g'
-  in res
+    List.map2
+      (fun c pat ->
+         ((None, ElimOnConstr (fun env sigma -> (sigma,(c,Tactypes.NoBindings)))),
+          (None,pat), None))
+      (args@c_list)
+      encoded_pat_as_patlist
+  in
+  let princ' = Some (princ,bindings) in
+  let princ_vars =
+    List.fold_right
+      (fun a acc -> try Id.Set.add (destVar sigma a) acc with DestKO -> acc)
+      args
+      Id.Set.empty
+  in
+  let old_idl = List.fold_right Id.Set.add (pf_ids_of_hyps gl) Id.Set.empty in
+  let old_idl = Id.Set.diff old_idl princ_vars in
+  let subst_and_reduce gl =
+    if with_clean
+    then
+      let idl = List.filter (fun id -> not (Id.Set.mem id old_idl))(pf_ids_of_hyps gl) in
+      let flag = Genredexpr.Cbv { Redops.all_flags with Genredexpr.rDelta = false } in
+      tclTHEN
+        (tclMAP (fun id -> tclTRY (Equality.subst_gen (do_rewrite_dependent ()) [id])) idl)
+        (reduce flag Locusops.allHypsAndConcl)
+    else tclIDTAC
+  in
+  tclTHEN
+    (choose_dest_or_ind
+       princ_infos
+       (args_as_induction_constr,princ'))
+    (Proofview.Goal.enter subst_and_reduce))
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 97a840e950..476d74b3f8 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -8,9 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val functional_induction :
-  bool ->
-  EConstr.constr ->
-  (EConstr.constr * EConstr.constr Tactypes.bindings) option ->
-  Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
-  Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
+val functional_induction
+  :  bool
+  -> EConstr.constr
+  -> (EConstr.constr * EConstr.constr Tactypes.bindings) option
+  -> Ltac_plugin.Tacexpr.or_and_intro_pattern option
+  -> unit Proofview.tactic
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 52a29fb559..7719705138 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -92,13 +92,6 @@ let list_union_eq eq_fun l1 l2 =
 let list_add_set_eq eq_fun x l =
   if List.exists (eq_fun x) l then l else x::l
 
-let const_of_id id =
-  let princ_ref = qualid_of_ident id in
-  try Constrintern.locate_reference princ_ref
-  with Not_found ->
-    CErrors.user_err ~hdr:"IndFun.const_of_id"
-      (str "cannot find " ++ Id.print id)
-
 [@@@ocaml.warning "-3"]
 let coq_constant s =
   UnivGen.constr_of_monomorphic_global @@
@@ -301,20 +294,16 @@ let find_or_none id =
     )
   with Not_found -> None
 
-
-
 let find_Function_infos f =
-  Cmap_env.find f !from_function
-
+  Cmap_env.find_opt f !from_function
 
 let find_Function_of_graph ind =
-  Indmap.find ind !from_graph
+  Indmap.find_opt ind !from_graph
 
 let update_Function finfo =
   (* Pp.msgnl (pr_info finfo); *)
   Lib.add_anonymous_leaf (in_Function finfo)
 
-
 let add_Function is_general f =
   let f_id = Label.to_id (Constant.label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index fff4711044..16beaaa3c7 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -38,7 +38,6 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 val make_eq : unit -> EConstr.constr
@@ -75,8 +74,8 @@ type function_info =
       is_general : bool;
     }
 
-val find_Function_infos : Constant.t -> function_info
-val find_Function_of_graph : inductive -> function_info
+val find_Function_infos : Constant.t -> function_info option
+val find_Function_of_graph : inductive -> function_info option
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> Constant.t -> unit
 val update_Function : function_info -> unit
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 38fdd789a3..d72319d078 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -34,9 +34,10 @@ let revert_graph kn post_tac hid = Proofview.Goal.enter (fun gl ->
     let ((kn',num) as ind'),u = destInd sigma i in
     if MutInd.equal kn kn'
     then (* We have generated a graph hypothesis so that we must change it if we can *)
-      let info =
-        try find_Function_of_graph ind'
-        with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*)
+      let info = match find_Function_of_graph ind' with
+        | Some info -> info
+        | None ->
+          (* The graphs are mutually recursive but we cannot find one of them !*)
           CErrors.anomaly (Pp.str "Cannot retrieve infos about a mutual block.")
       in
       (* if we can find a completeness lemma for this function
@@ -108,18 +109,20 @@ let invfun qhyp f  =
     | _ ->
       CErrors.user_err Pp.(str "Not a function")
   in
-  try
-    let finfos = find_Function_infos f in
-    let f_correct = mkConst(Option.get finfos.correctness_lemma)
-    and kn = fst finfos.graph_ind in
-    Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
-  with
-  | Not_found -> CErrors.user_err (Pp.str "No graph found")
-  | Option.IsNone  -> CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
-
-exception NoFunction
+  match find_Function_infos f with
+  | None ->
+    CErrors.user_err (Pp.str "No graph found")
+  | Some finfos ->
+    match finfos.correctness_lemma with
+    | None ->
+      CErrors.user_err (Pp.str "Cannot use equivalence with graph!")
+    | Some f_correct ->
+      let f_correct = mkConst f_correct
+      and kn = fst finfos.graph_ind in
+      Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f)  f_correct) qhyp
 
 let invfun qhyp f =
+  let exception NoFunction in
   match f with
   | Some f -> invfun qhyp f
   | None ->
@@ -132,31 +135,33 @@ let invfun qhyp f =
           let f1,_ = decompose_app sigma args.(1) in
           try
             if not (isConst sigma f1) then raise NoFunction;
-            let finfos = find_Function_infos (fst (destConst sigma f1)) in
+            let finfos = Option.get (find_Function_infos (fst (destConst sigma f1))) in
             let f_correct = mkConst(Option.get finfos.correctness_lemma)
             and kn = fst finfos.graph_ind
             in
             functional_inversion kn hid f1 f_correct
-          with | NoFunction | Option.IsNone | Not_found ->
-          try
-            let f2,_ = decompose_app sigma args.(2) in
-            if not (isConst sigma f2) then raise NoFunction;
-            let finfos = find_Function_infos (fst (destConst sigma f2)) in
-            let f_correct = mkConst(Option.get finfos.correctness_lemma)
-            and kn = fst finfos.graph_ind
-            in
-            functional_inversion kn hid  f2 f_correct
           with
-          | NoFunction ->
-            CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
-          | Option.IsNone  ->
-            if do_observe ()
-            then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
-            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
-          | Not_found ->
-            if do_observe ()
-            then CErrors.user_err (Pp.str "No graph found for any side of equality")
-            else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+          | NoFunction | Option.IsNone ->
+            let f2,_ = decompose_app sigma args.(2) in
+            if isConst sigma f2 then
+              match find_Function_infos (fst (destConst sigma f2)) with
+              | None ->
+                if do_observe ()
+                then CErrors.user_err (Pp.str "No graph found for any side of equality")
+                else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+              | Some finfos ->
+                match finfos.correctness_lemma with
+                | None ->
+                  if do_observe ()
+                  then CErrors.user_err (Pp.str "Cannot use equivalence with graph for any side of the equality")
+                  else CErrors.user_err Pp.(str "Cannot find inversion information for hypothesis " ++ Ppconstr.pr_id hid)
+                | Some f_correct ->
+                  let f_correct = mkConst f_correct
+                  and kn = fst finfos.graph_ind
+                  in
+                  functional_inversion kn hid  f2 f_correct
+            else                (* NoFunction *)
+              CErrors.user_err Pp.(str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function")
         end
       | _ -> CErrors.user_err Pp.(Ppconstr.pr_id hid ++ str " must be an equality ")
     in