aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/pbp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index e0f88ba69a..ef9f1280bc 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -40,7 +40,7 @@ let get_hyp_by_name g name =
(* je sais, c'est pas beau, mais je ne sais pas trop me servir de look_up...
Loïc *)
with _ -> (let c = Nametab.global (Ident (zz,name)) in
- ("cste",type_of (Global.env()) Evd.empty (constr_of_reference c)))
+ ("cste",type_of (Global.env()) Evd.empty (constr_of_global c)))
;;
type pbp_atom =