diff options
author | 2018-06-13 00:22:57 +0200 | |
---|---|---|
committer | 2018-06-18 11:02:58 +0200 | |
commit | 61c7a4be0e8ea8f0cc703ee3fed3bacfdf13116f (patch) | |
tree | c0d688ecee1d04f01f25a121cc3cc6ecabdfa1bc /plugins/ltac/g_tactic.ml4 | |
parent | f08153148b3ca0de01e5d7c68d5b318a2cae6d0d (diff) |
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.
Diffstat (limited to 'plugins/ltac/g_tactic.ml4')
-rw-r--r-- | plugins/ltac/g_tactic.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 05005c733..31bc34a32 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -156,7 +156,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then |