diff options
Diffstat (limited to 'plugins/ssr/ssrbwd.ml')
| -rw-r--r-- | plugins/ssr/ssrbwd.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml index f0ae90beca..ca92d70263 100644 --- a/plugins/ssr/ssrbwd.ml +++ b/plugins/ssr/ssrbwd.ml @@ -12,7 +12,6 @@ open Printer open Pretyping -open Globnames open Glob_term open Tacmach @@ -47,7 +46,7 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) = let loc = rc.CAst.loc in match DAst.get rc with | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' - | GRef (VarRef id, _) when not_section_id id -> + | GRef (Names.GlobRef.VarRef id, _) when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs' | _ -> clr', rcs' @@ -89,7 +88,7 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c) let apply_rconstr ?ist t gl = (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *) let n = match ist, DAst.get t with - | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) + | None, (GVar id | GRef (Names.GlobRef.VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id) | Some ist, _ -> interp_nbargs ist gl t | _ -> anomaly "apply_rconstr without ist and not RVar" in let mkRlemma i = mkRApp t (mkRHoles i) in |