diff options
Diffstat (limited to 'plugins/ltac/rewrite.ml')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 40 |
1 files changed, 17 insertions, 23 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index e8c9f4ebaa..966b11d0e7 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -55,22 +55,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else Coqlib.check_required_library ["Coq";"Setoids";"Setoid"] -let make_dir l = DirPath.make (List.rev_map Id.of_string l) +let lazy_find_reference dir s = + let gr = lazy (Coqlib.coq_reference "generalized rewriting" dir s) in + fun () -> Lazy.force gr -let try_find_global_reference dir s = - let sp = Libnames.make_path (make_dir ("Coq"::dir)) (Id.of_string s) in - try Nametab.global_of_path sp - with Not_found -> - anomaly (str "Global reference " ++ str s ++ str " not found in generalized rewriting") - -let find_reference dir s = - let gr = lazy (try_find_global_reference dir s) in - fun () -> Lazy.force gr +let find_reference dir s = Coqlib.coq_reference "generalized rewriting" dir s type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) let find_global dir s = - let gr = lazy (try_find_global_reference dir s) in + let gr = lazy (find_reference dir s) in fun (evd,cstrs) -> let sigma = Sigma.Unsafe.of_evar_map evd in let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in @@ -81,7 +75,7 @@ let find_global dir s = (** Global constants. *) -let coq_eq_ref = find_reference ["Init"; "Logic"] "eq" +let coq_eq_ref = lazy_find_reference ["Init"; "Logic"] "eq" let coq_eq = find_global ["Init"; "Logic"] "eq" let coq_f_equal = find_global ["Init"; "Logic"] "f_equal" let coq_all = find_global ["Init"; "Logic"] "all" @@ -158,11 +152,11 @@ end) = struct let forall_relation = find_global morphisms "forall_relation" let pointwise_relation = find_global morphisms "pointwise_relation" - let forall_relation_ref = find_reference morphisms "forall_relation" - let pointwise_relation_ref = find_reference morphisms "pointwise_relation" + let forall_relation_ref = lazy_find_reference morphisms "forall_relation" + let pointwise_relation_ref = lazy_find_reference morphisms "pointwise_relation" let respectful = find_global morphisms "respectful" - let respectful_ref = find_reference morphisms "respectful" + let respectful_ref = lazy_find_reference morphisms "respectful" let default_relation = find_global ["Classes"; "SetoidTactics"] "DefaultRelation" @@ -174,8 +168,8 @@ end) = struct let rewrite_relation_class = find_global relation_classes "RewriteRelation" - let proper_class = lazy (class_info (try_find_global_reference morphisms "Proper")) - let proper_proxy_class = lazy (class_info (try_find_global_reference morphisms "ProperProxy")) + let proper_class = lazy (class_info (find_reference morphisms "Proper")) + let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy")) let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) @@ -241,7 +235,7 @@ end) = struct let liftarg = mkLambda (na, ty, arg) in let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs - else error "build_signature: no constraint can apply on a dependent argument" + else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument") | _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products") | _, [] -> (match finalcstr with @@ -478,7 +472,7 @@ type hypinfo = { let get_symmetric_proof b = if b then PropGlobal.get_symmetric_proof else TypeGlobal.get_symmetric_proof -let error_no_relation () = error "Cannot find a relation to rewrite." +let error_no_relation () = user_err Pp.(str "Cannot find a relation to rewrite.") let rec decompose_app_rel env evd t = (** Head normalize for compatibility with the old meta mechanism *) @@ -531,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) = let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *) match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with | Some c -> c - | None -> error "Cannot find an homogeneous relation to rewrite." + | None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.") let rewrite_db = "rewrite" @@ -837,7 +831,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev sigargs, r.rew_to :: typeargs') | None -> if not (Option.is_empty y) then - error "Cannot rewrite inside dependent arguments of a function"; + user_err Pp.(str "Cannot rewrite inside dependent arguments of a function"); x :: acc, x :: subst, evars, sigargs, x :: typeargs') ([], [], evars, sigargs, []) args args' in @@ -1425,7 +1419,7 @@ module Strategies = let unfolded = try Tacred.try_red_product env sigma c with e when CErrors.noncritical e -> - error "fold: the term is not unfoldable !" + user_err Pp.(str "fold: the term is not unfoldable !") in try let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in @@ -2204,7 +2198,7 @@ let setoid_symmetry_in id = let rec split_last_two = function | [c1;c2] -> [],(c1, c2) | x::y::z -> let l,res = split_last_two (y::z) in x::l, res - | _ -> error "Cannot find an equivalence relation to rewrite." + | _ -> user_err Pp.(str "Cannot find an equivalence relation to rewrite.") in let others,(c1,c2) = split_last_two args in let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in |