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/firstorder/instances.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder/instances.ml')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 286021d68e..1c9ab2e3bd 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance env evmap id idc m t =
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
-	match nam with
+        match nam.Context.binder_name with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
@@ -115,7 +115,7 @@ let mk_open_instance env evmap id idc m t =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id_in_env avoid var_id env) in
       let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let decl = LocalAssum (Name nid, c) in
+      let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
 	aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m Id.Set.empty env evmap [] in
   (evmap, decls, revt)
-- 
cgit v1.2.3