diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0d279ae93d..f2ffb0413b 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -39,6 +39,10 @@ open Context.Named.Declaration module NamedDecl = Context.Named.Declaration module RelDecl = Context.Rel.Declaration +let local_assum (na, t) = + let inj = EConstr.Unsafe.to_constr in + RelDecl.LocalAssum (na, inj t) + (** Typeclass-based generalized rewriting. *) (** Constants used by the tactic. *) @@ -531,7 +535,8 @@ let decompose_applied_relation env sigma (c,l) = | Some c -> c | None -> let ctx,t' = Reductionops.splay_prod env sigma (EConstr.of_constr ctype) in (* Search for underlying eq *) - match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with + let t' = EConstr.Unsafe.to_constr t' in + match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> local_assum (n, t)) ctx)) with | Some c -> c | None -> error "Cannot find an homogeneous relation to rewrite." |