From 416cccb2b0c7db284130723ef1c2f3851b995ae9 Mon Sep 17 00:00:00 2001
From: Andreas Lynge
Date: Tue, 21 May 2019 20:37:42 +0200
Subject: Make discriminate tactic compatible with HoTT

---
 plugins/ltac/rewrite.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 5db8f999e5..775d3969db 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -947,9 +947,9 @@ let fold_match ?(force=false) env sigma c =
 	  if dep then case_dep_scheme_kind_from_prop
 	  else case_scheme_kind_from_prop
 	else (
-	  if dep
-	  then case_dep_scheme_kind_from_type_in_prop
-	  else case_scheme_kind_from_type)
+          if dep
+          then case_dep_scheme_kind_from_type_in_prop
+          else case_scheme_kind_from_type)
       else ((* sortc <> InProp by typing *)
 	if dep
 	then case_dep_scheme_kind_from_type
-- 
cgit v1.2.3