diff options
| -rw-r--r-- | pretyping/unification.ml | 2 | ||||
| -rw-r--r-- | tactics/rewrite.ml | 39 |
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 *) |