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 /kernel/cbytegen.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 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 1d2587efe..021e50847 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -188,7 +188,7 @@ let find_at f l = let pos_named id r = let env = !(r.in_env) in let cid = FVnamed id in - let f = function FVnamed id' -> id_eq id id' | _ -> false in + let f = function FVnamed id' -> Id.equal id id' | _ -> false in try Kenvacc(r.offset + env.size - (find_at f env.fv_rev)) with Not_found -> let pos = env.size in @@ -710,7 +710,7 @@ let compile env c = Format.print_string "fv = "; List.iter (fun v -> match v with - | FVnamed id -> Format.print_string ((string_of_id id)^"; ") + | FVnamed id -> Format.print_string ((Id.to_string id)^"; ") | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format .print_string "\n"; Format.print_flush(); *) |