diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-04 18:58:27 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-06 23:05:31 +0100 |
| commit | f3abbc55ef160d1a65d4467bfe9b25b30b965a46 (patch) | |
| tree | fceac407f6e4254e107817b6140257bcc8f9755a /tactics/equality.ml | |
| parent | 0d81e80a09db7d352408be4dfc5ba263f6ed98ef (diff) | |
[api] Deprecate all legacy uses of Names in core.
This will allow to merge back `Names` with `API.Names`
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c03a3ba6..881000219 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -374,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot = | Some true, None | Some false, Some _ -> let c1 = destConstRef pr1 in - let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in + let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in + let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in begin try let _ = Global.lookup_constant c1' in c1' with Not_found -> user_err ~hdr:"Equality.find_elim" - (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") + (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end | _ -> destConstRef pr1 end |