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

---
 plugins/funind/functional_principles_proofs.ml |  4 ++--
 plugins/funind/gen_principle.ml                |  4 ++--
 plugins/funind/recdef.ml                       | 23 +++++++++++++++--------
 3 files changed, 19 insertions(+), 12 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9b578d4697..f2658a395f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -585,10 +585,10 @@ let build_proof (interactive_proof : bool) (fnames : Constant.t list) ptes_infos
     let sigma = project g in
     (*      observe (str "proving on " ++ Printer.pr_lconstr_env (pf_env g) term);*)
     match EConstr.kind sigma dyn_infos.info with
-    | Case (ci, ct, t, cb) ->
+    | Case (ci, ct, iv, t, cb) ->
       let do_finalize_t dyn_info' g =
         let t = dyn_info'.info in
-        let dyn_infos = {dyn_info' with info = mkCase (ci, ct, t, cb)} in
+        let dyn_infos = {dyn_info' with info = mkCase (ci, ct, iv, t, cb)} in
         let g_nb_prod = nb_prod (project g) (pf_concl g) in
         let g, type_of_term = tac_type_of g t in
         let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 167cf37026..d09609bf7a 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -987,7 +987,7 @@ and intros_with_rewrite_aux : Tacmach.tactic =
                   ( UnivGen.constr_of_monomorphic_global
                   @@ Coqlib.lib_ref "core.False.type" )) ->
         Proofview.V82.of_tactic tauto g
-      | Case (_, _, v, _) ->
+      | Case (_, _, _, v, _) ->
         tclTHENLIST
           [Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite]
           g
@@ -1026,7 +1026,7 @@ let rec reflexivity_with_destruct_cases g =
       match
         EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2)
       with
-      | Case (_, _, v, _) ->
+      | Case (_, _, _, v, _) ->
         tclTHENLIST
           [ Proofview.V82.of_tactic (simplest_case v)
           ; Proofview.V82.of_tactic intros
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 884792cc15..701ea56c2a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -312,7 +312,7 @@ let check_not_nested env sigma forbidden e =
     | Const _ -> ()
     | Ind _ -> ()
     | Construct _ -> ()
-    | Case (_, t, e, a) ->
+    | Case (_, t, _, e, a) ->
       check_not_nested t;
       check_not_nested e;
       Array.iter check_not_nested a
@@ -374,7 +374,13 @@ type journey_info =
   ; lambdA : (Name.t * types * constr, constr) journey_info_tac
   ; casE :
          ((constr infos -> tactic) -> constr infos -> tactic)
-      -> (case_info * constr * constr * constr array, constr) journey_info_tac
+      -> ( case_info
+           * constr
+           * (constr, EInstance.t) case_invert
+           * constr
+           * constr array
+         , constr )
+         journey_info_tac
   ; otherS : (unit, constr) journey_info_tac
   ; apP : (constr * constr list, constr) journey_info_tac
   ; app_reC : (constr * constr list, constr) journey_info_tac
@@ -474,9 +480,9 @@ let rec travel_aux jinfo continuation_tac (expr_info : constr infos) g =
         ++ Printer.pr_leconstr_env env sigma expr_info.info
         ++ str " can not contain a recursive call to "
         ++ Id.print expr_info.f_id ) )
-  | Case (ci, t, a, l) ->
+  | Case (ci, t, iv, a, l) ->
     let continuation_tac_a =
-      jinfo.casE (travel jinfo) (ci, t, a, l) expr_info continuation_tac
+      jinfo.casE (travel jinfo) (ci, t, iv, a, l) expr_info continuation_tac
     in
     travel jinfo continuation_tac_a
       {expr_info with info = a; is_main_branch = false; is_final = false}
@@ -767,7 +773,8 @@ let mkDestructEq not_on_hyp expr g =
   in
   (g, tac, to_revert)
 
-let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
+let terminate_case next_step (ci, a, iv, t, l) expr_info continuation_tac infos
+    g =
   let sigma = project g in
   let env = pf_env g in
   let f_is_present =
@@ -779,7 +786,7 @@ let terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos g =
   let a' = infos.info in
   let new_info =
     { infos with
-      info = mkCase (ci, t, a', l)
+      info = mkCase (ci, t, iv, a', l)
     ; is_main_branch = expr_info.is_main_branch
     ; is_final = expr_info.is_final }
   in
@@ -916,10 +923,10 @@ let prove_terminate = travel terminate_info
 
 (* Equation proof *)
 
-let equation_case next_step (ci, a, t, l) expr_info continuation_tac infos =
+let equation_case next_step case expr_info continuation_tac infos =
   observe_tac
     (fun _ _ -> str "equation case")
-    (terminate_case next_step (ci, a, t, l) expr_info continuation_tac infos)
+    (terminate_case next_step case expr_info continuation_tac infos)
 
 let rec prove_le g =
   let sigma = project g in
-- 
cgit v1.2.3