diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /library/globnames.ml | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/globnames.ml')
| -rw-r--r-- | library/globnames.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/globnames.ml b/library/globnames.ml index b5312e574..9ce5451a1 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -29,7 +29,7 @@ let eq_gr gr1 gr2 = | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 - | VarRef v1, VarRef v2 -> id_eq v1 v2 + | VarRef v1, VarRef v2 -> Id.equal v1 v2 | _ -> false let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" @@ -87,7 +87,7 @@ let global_ord_gen fc fmi x y = | ConstructRef (indx,jx), ConstructRef (indy,jy) -> let c = Int.compare jx jy in if Int.equal c 0 then ind_ord indx indy else c - | VarRef v1, VarRef v2 -> id_ord v1 v2 + | VarRef v1, VarRef v2 -> Id.compare v1 v2 | _, _ -> Pervasives.compare x y let global_ord_can = global_ord_gen canonical_con canonical_mind |