aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/detyping.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:27:09 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-06 23:46:52 +0100
commit03e21974a3e971a294533bffb81877dc1bd270b6 (patch)
tree1b37339378f6bc93288b61f707efb6b08f992dc5 /pretyping/detyping.ml
parentf3abbc55ef160d1a65d4467bfe9b25b30b965a46 (diff)
[api] Move structures deprecated in the API to the core.
We do up to `Term` which is the main bulk of the changes.
Diffstat (limited to 'pretyping/detyping.ml')
-rw-r--r--pretyping/detyping.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c02fc5aaf..0d1e401d9 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -554,7 +554,7 @@ and detype_r d flags avoid env sigma t =
let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel sigma c && Int.Set.mem (destRel sigma c) rels || isVar sigma c && (Id.Set.mem (destVar sigma c) fvs)))) (Evd.find sigma evk) cl in
id,l
with Not_found ->
- Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
+ Id.of_string ("X" ^ string_of_int (Evar.repr evk)),
(Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
in
GEvar (id,