aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3a9dc3a75..89d4e57ae 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -530,7 +530,7 @@ let find_constructor ref =
let rec unf = function
| ConstRef cst ->
let v = Environ.constant_value (Global.env()) cst in
- unf (reference_of_constr v)
+ unf (global_of_constr v)
| ConstructRef c ->
if !dump then add_glob loc r;
c, []