diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 21:41:41 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 01:38:53 +0200 |
commit | 8ab00e5f272aa8f16d70a00323c57f2d4ef66f03 (patch) | |
tree | 337344749e72cc85334bfb56769272edf3e9b21d /pretyping/cases.ml | |
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 'pretyping/cases.ml')
-rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2c8065a9..f16f393f6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -731,7 +731,7 @@ let get_names env sigma sign eqns = (fun (LocalAssum (na,t) | LocalDef (na,_,t)) -> Name (next_name_away (named_hd env sigma t na) avoid)) d na in - (na::l,(out_name na)::avoid)) + (na::l,(Name.get_id na)::avoid)) ([],allvars) (List.rev sign) names2 in names3,aliasname |