From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 interp/constrintern.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'interp/constrintern.ml')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index cb50245d5a..c87768b190 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2059,6 +2059,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     | CProj (pr, c) ->
       match intern_reference pr with
       | ConstRef p ->
+        let p = Option.get @@ Recordops.find_primitive_projection p in
         DAst.make ?loc @@ GProj (Projection.make p false, intern env c)
       | _ ->
         raise (InternalizationError (loc,IllegalMetavariable)) (* FIXME *)
-- 
cgit v1.2.3