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/rules.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

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

diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 832a98b7f8..7f06ab6777 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -163,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
   let open Vars in
-  let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d idc = mkLambda (Anonymous,b,
-		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+  let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in
+  let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b,
+                  mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (cut c)
 	 [tclTHENLIST
-- 
cgit v1.2.3