From c5ecebf6fefbaa673dda506175a2aa4a69d79807 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Sep 2014 00:03:46 +0200
Subject: Revert specific syntax for primitive projections, avoiding ugly
 contortions in internalization/externalization. It uses a fully typed version
 of detyping, requiring the environment, to move from primitive projection
 applications to regular applications of the eta-expanded version. The kernel
 is unchanged, and only constrMatching needs compatibility code now.

---
 plugins/firstorder/instances.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2987ce60a1..80576212fd 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] evmap nt in
+  let rawt=Detyping.detype false [] env evmap nt in
   let rec raux n t=
     if Int.equal n 0 then t else
       match t with
-- 
cgit v1.2.3