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/evarconv.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/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index bf62cea6b..630f80ad2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -638,7 +638,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] and f2 i = @@ -755,7 +755,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max na1 na2 in + let na = Nameops.Name.pick na1 na2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -816,7 +816,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty [(fun i -> evar_conv_x ts env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in - let na = Nameops.name_max n1 n2 in + let na = Nameops.Name.pick n1 n2 in evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> |