diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 94ec0a898a..d68bdc2153 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -7,7 +7,6 @@ (************************************************************************) open Ltac_plugin -open Tacexpr open Declarations open CErrors open Util @@ -31,8 +30,8 @@ module RelDecl = Context.Rel.Declaration let pr_binding prc = function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (NamedHyp id, c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | ImplicitBindings l -> @@ -198,7 +197,7 @@ let generate_type evd g_to_f f graph i = let find_induction_principle evd f = let f_as_constant,u = match EConstr.kind !evd f with | Const c' -> c' - | _ -> error "Must be used with a function" + | _ -> 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 @@ -274,7 +273,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.map (fun decl -> List.map - (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) + (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -547,7 +546,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ @@ -702,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> error "No graph found" + with Not_found -> user_err Pp.(str "No graph found") in if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs @@ -1007,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic = | _ -> tclFAIL 1 (mt ()) g +let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = @@ -1026,7 +1026,7 @@ let invfun qhyp f = | Not_found -> error "No graph found" | Option.IsNone -> error "Cannot use equivalence with graph!" - +exception NoFunction let invfun qhyp f g = match f with | Some f -> invfun qhyp f g @@ -1041,23 +1041,23 @@ let invfun qhyp f g = begin let f1,_ = decompose_app sigma args.(1) in try - if not (isConst sigma f1) then failwith ""; + if not (isConst sigma f1) then raise NoFunction; let finfos = 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 g - with | Failure "" | Option.IsNone | Not_found -> + with | NoFunction | Option.IsNone | Not_found -> try let f2,_ = decompose_app sigma args.(2) in - if not (isConst sigma f2) then failwith ""; + 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 g with - | Failure "" -> + | NoFunction -> user_err (str "Hypothesis " ++ Ppconstr.pr_id hid ++ str " must contain at least one Function") | Option.IsNone -> if do_observe () |