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

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 4664df3182..1981e24ae4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -352,8 +352,8 @@ let named_of_rel_context l =
       (fun decl (subst, ctx) ->
         let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
 	let d = match decl with
-	  | LocalAssum (_,t) -> id, None, substl subst t
-	  | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+          | LocalAssum (_,t) -> id, None, substl subst t
+          | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
 	  (mkVar id :: subst, d :: ctx))
       l ([], [])
   in ctx
-- 
cgit v1.2.3