From 23f84f37c674a07e925925b7e0d50d7ee8414093 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 31 Oct 2017 17:04:02 +0100
Subject: Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.
---
 plugins/derive/derive.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/derive')

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index d06a241969..afdbfa1999 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Constr
+open Context
 open Context.Named.Declaration
 
 let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body)
@@ -39,7 +40,7 @@ let start_deriving f suchthat lemma =
         TCons ( env , sigma , f_type , (fun sigma ef ->
         let f_type = EConstr.Unsafe.to_constr f_type in
         let ef = EConstr.Unsafe.to_constr ef in
-        let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in
+        let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
         let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
         TCons ( env' , sigma , suchthat , (fun sigma _ ->
         TNil sigma))))))
-- 
cgit v1.2.3