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

(limited to 'plugins/ltac/tauto.ml')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 19256e054d..4c65445b89 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -142,7 +142,7 @@ let flatten_contravariant_conj _ ist =
           ~onlybinary:flags.binary_mode typ
   with
   | Some (_,args) ->
-    let newtyp = List.fold_right mkArrow args c in
+    let newtyp = List.fold_right (fun a b -> mkArrow a Sorts.Relevant b) args c in
     let intros = tclMAP (fun _ -> intro) args in
     let by = tclTHENLIST [intros; apply hyp; split; assumption] in
     tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)]
@@ -173,7 +173,7 @@ let flatten_contravariant_disj _ ist =
           typ with
   | Some (_,args) ->
       let map i arg =
-        let typ = mkArrow arg c in
+        let typ = mkArrow arg Sorts.Relevant c in
         let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in
         let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
         assert_ ~by typ
-- 
cgit v1.2.3