From 2ded4c25e532c5dfca0483c211653768ebed01a7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 13 Jun 2019 15:39:43 +0200
Subject: UIP in SProp

---
 checker/checkFlags.ml | 1 +
 checker/checker.ml    | 1 +
 checker/values.ml     | 5 +++--
 3 files changed, 5 insertions(+), 2 deletions(-)

(limited to 'checker')

diff --git a/checker/checkFlags.ml b/checker/checkFlags.ml
index 1f5e76bd83..369623e8c5 100644
--- a/checker/checkFlags.ml
+++ b/checker/checkFlags.ml
@@ -18,6 +18,7 @@ let set_local_flags flags env =
       check_universes = flags.check_universes;
       conv_oracle = flags.conv_oracle;
       cumulative_sprop = flags.cumulative_sprop;
+      allow_uip = flags.allow_uip;
     }
   in
   Environ.set_typing_flags flags env
diff --git a/checker/checker.ml b/checker/checker.ml
index 086acc482c..ab0ea41a36 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -299,6 +299,7 @@ let explain_exn = function
       | UnsatisfiedConstraints _ -> str"UnsatisfiedConstraints"
       | DisallowedSProp -> str"DisallowedSProp"
       | BadRelevance -> str"BadRelevance"
+      | BadInvert -> str"BadInvert"
       | UndeclaredUniverse _ -> str"UndeclaredUniverse"))
 
   | InductiveError e ->
diff --git a/checker/values.ml b/checker/values.ml
index cce0ce7203..178a3d8624 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -147,7 +147,7 @@ let rec v_constr =
     [|v_puniverses v_cst|]; (* Const *)
     [|v_puniverses v_ind|]; (* Ind *)
     [|v_puniverses v_cons|]; (* Construct *)
-    [|v_caseinfo;v_constr;v_constr;Array v_constr|]; (* Case *)
+    [|v_caseinfo;v_constr;v_case_invert;v_constr;Array v_constr|]; (* Case *)
     [|v_fix|]; (* Fix *)
     [|v_cofix|]; (* CoFix *)
     [|v_proj;v_constr|]; (* Proj *)
@@ -159,6 +159,7 @@ and v_prec = Tuple ("prec_declaration",
                     [|Array (v_binder_annot v_name); Array v_constr; Array v_constr|])
 and v_fix = Tuple ("pfixpoint", [|Tuple ("fix2",[|Array Int;Int|]);v_prec|])
 and v_cofix = Tuple ("pcofixpoint",[|Int;v_prec|])
+and v_case_invert = Sum ("case_inversion", 1, [|[|v_instance;Array v_constr|]|])
 
 let v_rdecl = v_sum "rel_declaration" 0
     [| [|v_binder_annot v_name; v_constr|];               (* LocalAssum *)
@@ -244,7 +245,7 @@ let v_typing_flags =
   v_tuple "typing_flags"
     [|v_bool; v_bool; v_bool;
       v_oracle; v_bool; v_bool;
-      v_bool; v_bool; v_bool|]
+      v_bool; v_bool; v_bool; v_bool|]
 
 let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
-- 
cgit v1.2.3