diff options
| author | Hugo Herbelin | 2017-04-13 21:41:41 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 01:38:53 +0200 |
| commit | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch) | |
| tree | 337344749e72cc85334bfb56769272edf3e9b21d /tactics | |
| parent | 4865160fa1f2e9ce03b37b9cb3ac99c35e9c4e4d (diff) | |
Creating a module Nameops.Name extending module Names.Name.
This module collects the functions of Nameops which are about Name.t
and somehow standardize or improve their name, resulting in particular
from discussions in working group.
Note the use of a dedicated exception rather than a failwith for
Nameops.Name.out.
Drawback of the approach: one needs to open Nameops, or to use long
prefix Nameops.Name.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e8cb4e632..85971e6650 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2975,7 +2975,7 @@ let specialize (c,lbind) ipat = if occur_meta clause.evd term then user_err (str "Cannot infer an instance for " ++ - pr_name (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ + Name.print (meta_name clause.evd (List.hd (collect_metas clause.evd term))) ++ str "."); clause.evd, term in let typ = Retyping.get_type_of env sigma term in |