diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 86defb2f2f..d4cc31c0af 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -19,7 +19,6 @@ open Context open EConstr open Vars open Pp -open Globnames open Tacticals open Tactics open Indfun_common @@ -54,9 +53,8 @@ let do_observe_tac s tac g = msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v with reraise -> let reraise = CErrors.push reraise in - let e = ExplainErr.process_vernac_interp_error reraise in observe (hov 0 (str "observation "++ s++str " raised exception " ++ - CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal )); + CErrors.iprint reraise ++ str " on goal" ++ fnl() ++ goal )); iraise reraise;; let observe_tac s tac g = @@ -94,7 +92,7 @@ let make_eq () = let generate_type evd g_to_f f graph i = (*i we deduce the number of arguments of the function and its returned type from the graph i*) let evd',graph = - Evd.fresh_global (Global.env ()) !evd (Globnames.IndRef (fst (destInd !evd graph))) + Evd.fresh_global (Global.env ()) !evd (GlobRef.IndRef (fst (destInd !evd graph))) in evd:=evd'; let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in @@ -166,7 +164,7 @@ let find_induction_principle evd f = match infos.rect_lemma with | None -> raise Not_found | Some rect_lemma -> - let evd',rect_lemma = Evd.fresh_global (Global.env ()) !evd (Globnames.ConstRef rect_lemma) in + 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 @@ -805,7 +803,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let (typ,_) = lemmas_types_infos.(i) in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in + ~kind:(Decls.(IsProof Theorem)) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false @@ -871,7 +869,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list let lem_id = mk_complete_id f_id in let info = Lemmas.Info.make ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decl_kinds.(Proof Theorem) () in + ~kind:Decls.(IsProof Theorem) () in let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info sigma (fst lemmas_types_infos.(i)) in let lemma = fst (Lemmas.by @@ -979,7 +977,7 @@ let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = match f with - | ConstRef f -> f + | GlobRef.ConstRef f -> f | _ -> raise (CErrors.UserError(None,str "Not a function")) in try |