From 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 13 Jun 2018 00:22:57 +0200 Subject: Remove reference name type. reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid. --- interp/implicit_quantifiers.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'interp/implicit_quantifiers.ml') diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b54e2badd..83ad9af33 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -96,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match CAst.(c.v) with - | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> - Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | CRef (qid,_) when qualid_is_ident qid -> + found c.CAst.loc (qualid_basename qid) bdvars l + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -196,7 +198,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid) + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -218,9 +220,8 @@ let destClassAppExpl cl = let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in - let qid = qualid_of_reference r in - let gr = Nametab.locate qid.CAst.v in + let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in + let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in -- cgit v1.2.3