aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--pretyping/unification.ml2
-rw-r--r--tactics/rewrite.ml39
2 files changed, 22 insertions, 19 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 236dc9876..58296002f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -126,7 +126,7 @@ let rec subst_meta_instances bl c =
let evar_source_of_meta mv evd =
match Evd.meta_name evd mv with
- | Anonymous -> assert false (* only dependent metas posed as evars (?) *)
+ | Anonymous -> (Loc.ghost,Evar_kinds.GoalEvar)
| Name id -> (Loc.ghost,Evar_kinds.VarInstance id)
let pose_all_metas_as_evars env evd t =
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 477e5bcda..d7091b5d0 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -352,6 +352,26 @@ end) = struct
| None -> None
| Some codom -> Some (decomp_pointwise 1 codom)
+ (** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
+ let is_applied_rewrite_relation env sigma rels t =
+ match kind_of_term t with
+ | App (c, args) when Array.length args >= 2 ->
+ let head = if isApp c then fst (destApp c) else c in
+ if Globnames.is_global (coq_eq_ref ()) head then None
+ else
+ (try
+ let params, args = Array.chop (Array.length args - 2) args in
+ let env' = Environ.push_rel_context rels env in
+ let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
+ let evars, inst =
+ app_poly env (evars,Evar.Set.empty)
+ rewrite_relation_class [| evar; mkApp (c, params) |] in
+ let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
+ Some (it_mkProd_or_LetIn t rels)
+ with e when Errors.noncritical e -> None)
+ | _ -> None
+
+
end
(* let my_type_of env evars c = Typing.e_type_of env evars c *)
@@ -410,24 +430,7 @@ end
let sort_of_rel env evm rel =
Reductionops.sort_of_arity env evm (Retyping.get_type_of env evm rel)
-(** Looking up declared rewrite relations (instances of [RewriteRelation]) *)
-let is_applied_rewrite_relation env sigma rels t =
- match kind_of_term t with
- | App (c, args) when Array.length args >= 2 ->
- let head = if isApp c then fst (destApp c) else c in
- if Globnames.is_global (coq_eq_ref ()) head then None
- else
- (try
- let params, args = Array.chop (Array.length args - 2) args in
- let env' = Environ.push_rel_context rels env in
- let evars, (evar, _) = Evarutil.new_type_evar Evd.univ_flexible sigma env' in
- let evars, inst =
- app_poly_check env (evars,Evar.Set.empty)
- TypeGlobal.rewrite_relation_class [| evar; mkApp (c, params) |] in
- let _ = Typeclasses.resolve_one_typeclass env' (goalevars evars) inst in
- Some (it_mkProd_or_LetIn t rels)
- with e when Errors.noncritical e -> None)
- | _ -> None
+let is_applied_rewrite_relation = PropGlobal.is_applied_rewrite_relation
(* let _ = *)
(* Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation *)