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.
---
 vernac/comAssumption.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'vernac/comAssumption.ml')

diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 35d8be5c56..37a33daf8f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -13,6 +13,7 @@ open Util
 open Vars
 open Declare
 open Names
+open Context
 open Globnames
 open Constrexpr_ops
 open Constrintern
@@ -148,8 +149,9 @@ let do_assumptions ~program_mode kind nl l =
   (* We intepret all declarations in the same evar_map, i.e. as a telescope. *)
   let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) ->
     let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in
+    let r = Retyping.relevance_of_type env sigma t in
     let env =
-      EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in
+      EConstr.push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (make_annot id r,t)) idl) env in
     let ienv = List.fold_right (fun {CAst.v=id} ienv ->
       let impls = compute_internalization_data env sigma Variable t imps in
       Id.Map.add id impls ienv) idl ienv in
-- 
cgit v1.2.3