- let term = disambiguate_term status_ref goal t in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+ let metasenv,term = disambiguate_term context metasenv t in
+ let pattern = disambiguate_pattern pattern in
+ metasenv,GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | GrafiteAst.Right loc ->
+ metasenv,GrafiteAst.Right loc
+ | GrafiteAst.Ring loc ->
+ metasenv,GrafiteAst.Ring loc
+ | GrafiteAst.Split loc ->
+ metasenv,GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc ->
+ metasenv,GrafiteAst.Symmetry loc