UIP in SProp

5 files changed, 29 insertions, 21 deletions

diff --git a/tactics/cbn.ml b/tactics/cbn.ml
index 21e38df6db..74f793cdfb 100644
--- a/tactics/cbn.ml
+++ b/tactics/cbn.ml
@@ -106,7 +106,7 @@ sig
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * Cst_stack.t
+  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -158,7 +158,7 @@ struct
 
   type 'a member =
   | App of 'a app_node
-  | Case of case_info * 'a * 'a array * Cst_stack.t
+  | Case of case_info * 'a * ('a, EInstance.t) case_invert * 'a array * Cst_stack.t
   | Proj of Projection.t * Cst_stack.t
   | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t
   | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t
@@ -172,7 +172,7 @@ struct
     let pr_c x = hov 1 (pr_c x) in
     match member with
     | App app -> str "ZApp" ++ pr_app_node pr_c app
-    | Case (_,_,br,cst) ->
+    | Case (_,_,_,br,cst) ->
        str "ZCase(" ++
          prvect_with_sep (pr_bar) pr_c br
        ++ str ")"
@@ -236,7 +236,7 @@ struct
         let t1,s1' = decomp_node_last a1 s1 in
         let t2,s2' = decomp_node_last a2 s2 in
         (f t1 t2) && (equal_rec s1' s2')
-      | Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
+      | Case (_,t1,_,a1,_) :: s1, Case (_,t2,_,a2,_) :: s2 ->
         f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
       | (Proj (p,_)::s1, Proj(p2,_)::s2) ->
         Projection.Repr.equal (Projection.repr p) (Projection.repr p2)
@@ -284,7 +284,7 @@ struct
 
   let will_expose_iota args =
     List.exists
-      (function (Fix (_,_,l) | Case (_,_,_,l) |
+      (function (Fix (_,_,l) | Case (_,_,_,_,l) |
                  Proj (_,l) | Cst (_,_,_,_,l)) when Cst_stack.is_empty l -> true | _ -> false)
       args
 
@@ -346,9 +346,9 @@ struct
                 then a
                 else Array.sub a i (j - i + 1) in
        zip (mkApp (f, a'), s)
-    | f, (Case (ci,rt,br,cst_l)::s) when refold ->
-      zip (best_state sigma (mkCase (ci,rt,f,br), s) cst_l)
-    | f, (Case (ci,rt,br,_)::s) -> zip (mkCase (ci,rt,f,br), s)
+    | f, (Case (ci,rt,iv,br,cst_l)::s) when refold ->
+      zip (best_state sigma (mkCase (ci,rt,iv,f,br), s) cst_l)
+    | f, (Case (ci,rt,iv,br,_)::s) -> zip (mkCase (ci,rt,iv,f,br), s)
     | f, (Fix (fix,st,cst_l)::s) when refold ->
       zip (best_state sigma (mkFix fix, st @ (append_app [|f|] s)) cst_l)
   | f, (Fix (fix,st,_)::s) -> zip
@@ -699,8 +699,8 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
         | _ -> fold ())
       | _ -> fold ())
 
-    | Case (ci,p,d,lf) ->
-      whrec Cst_stack.empty (d, Stack.Case (ci,p,lf,cst_l) :: stack)
+    | Case (ci,p,iv,d,lf) ->
+      whrec Cst_stack.empty (d, Stack.Case (ci,p,iv,lf,cst_l) :: stack)
 
     | Fix ((ri,n),_ as f) ->
       (match Stack.strip_n_app ri.(n) stack with
@@ -713,7 +713,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
       let use_fix = CClosure.RedFlags.red_set flags CClosure.RedFlags.fFIX in
       if use_match || use_fix then
         match Stack.strip_app stack with
-        |args, (Stack.Case(ci, _, lf,_)::s') when use_match ->
+        |args, (Stack.Case(ci, _, _, lf,_)::s') when use_match ->
           whrec Cst_stack.empty (lf.(c-1), (Stack.tail ci.ci_npar args) @ s')
         |args, (Stack.Proj (p,_)::s') when use_match ->
           whrec Cst_stack.empty (Stack.nth args (Projection.npars p + Projection.arg p), s')
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 6da2248cc3..955a7957bf 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -221,6 +221,7 @@ let build_sym_scheme env ind =
           [Context.Rel.to_extended_vect mkRel (3*nrealargs+2) paramsctxt1;
            rel_vect 1 nrealargs;
            rel_vect (2*nrealargs+2) nrealargs])),
+           NoInvert,
      mkRel 1 (* varH *),
        [|cstr (nrealargs+1)|]))))
   in c, UState.of_context_set ctx
@@ -295,6 +296,7 @@ let build_sym_involutive_scheme env ind =
                  rel_vect 1 nrealargs;
                  [|mkRel 1|]])|]]);
                mkRel 1|])),
+               NoInvert,
                mkRel 1 (* varH *),
                [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
   in (c, UState.of_context_set ctx)
@@ -434,9 +436,11 @@ let build_l2r_rew_scheme dep env ind kind =
                [|mkRel 2|]])|]]) in
   let main_body =
     mkCase (ci,
-      my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
-      applied_sym_C 3,
-      [|mkVar varHC|]) in
+            my_it_mkLambda_or_LetIn_name realsign_ind_G applied_PG,
+            NoInvert,
+            applied_sym_C 3,
+            [|mkVar varHC|])
+  in
   let c =
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign
@@ -444,12 +448,13 @@ let build_l2r_rew_scheme dep env ind kind =
     (my_it_mkProd_or_LetIn (if dep then realsign_ind_P else realsign_P) s)
   (mkNamedLambda (make_annot varHC indr) applied_PC
   (mkNamedLambda (make_annot varH indr) (lift 2 applied_ind)
-  (if dep then (* we need a coercion *)
+     (if dep then (* we need a coercion *)
      mkCase (cieq,
        mkLambda (make_annot (Name varH) indr,lift 3 applied_ind,
          mkLambda (make_annot Anonymous indr,
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
+       NoInvert,
        mkApp (sym_involutive,
          Array.append (Context.Rel.to_extended_vect mkRel 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
@@ -540,6 +545,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
          (my_it_mkProd_or_LetIn
            (if dep then realsign_ind_P 2 applied_ind_P else realsign_P 2) s)
        (mkNamedProd (make_annot varHC indr) applied_PC applied_PG)),
+     NoInvert,
      (mkVar varH),
      [|mkNamedLambda (make_annot varP indr)
         (my_it_mkProd_or_LetIn
@@ -616,6 +622,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
        my_it_mkLambda_or_LetIn_name
          (lift_rel_context (nrealargs+3) realsign_ind)
          (mkArrow applied_PG indr (lift (2*nrealargs+5) applied_PC)),
+       NoInvert,
        mkRel 3 (* varH *),
        [|mkLambda
           (make_annot (Name varHC) indr,
@@ -830,6 +837,7 @@ let build_congr env (eq,refl,ctx) ind =
               [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
                 mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
+       NoInvert,
        mkVar varH,
        [|mkApp (refl,
           [|mkVar varB;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 3aa7626aaa..a2325b69cc 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -877,7 +877,7 @@ let injectable env sigma ~keep_proofs t1 t2 =
  *)
 
 let descend_then env sigma head dirn =
-  let IndType (indf,_) =
+  let IndType (indf,_) as indt =
     try find_rectype env sigma (get_type_of env sigma head)
     with Not_found ->
       user_err Pp.(str "Cannot project on an inductive type derived from a dependency.")
@@ -904,7 +904,7 @@ let descend_then env sigma head dirn =
           (List.interval 1 (Array.length mip.mind_consnames)) in
       let rci = Sorts.Relevant in (* TODO relevance *)
       let ci = make_case_info env ind rci RegularStyle in
-      Inductiveops.make_case_or_project env sigma indf ci p head (Array.of_list brl)))
+      Inductiveops.make_case_or_project env sigma indt ci p head (Array.of_list brl)))
 
 (* Now we need to construct the discriminator, given a discriminable
    position.  This boils down to:
@@ -924,7 +924,7 @@ let descend_then env sigma head dirn =
    branch giving [special], and all the rest giving [default]. *)
 
 let build_selector env sigma dirn c ind special default =
-  let IndType(indf,_) =
+  let IndType(indf,_) as indt =
     try find_rectype env sigma ind
     with Not_found ->
        (* one can find Rel(k) in case of dependent constructors
@@ -950,7 +950,7 @@ let build_selector env sigma dirn c ind special default =
     List.map build_branch(List.interval 1 (Array.length mip.mind_consnames)) in
   let rci = Sorts.Relevant in (* TODO relevance *)
   let ci = make_case_info env ind rci RegularStyle in
-  let ans = Inductiveops.make_case_or_project env sigma indf ci p c (Array.of_list brl) in
+  let ans = Inductiveops.make_case_or_project env sigma indt ci p c (Array.of_list brl) in
   ans
 
 let build_coq_False () = pf_constr_of_global (lib_ref "core.False.type")
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 7a5615dd8e..386224824f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -562,7 +562,7 @@ struct
   let head_evar sigma c =
     let rec hrec c = match EConstr.kind sigma c with
       | Evar (evk,_)   -> evk
-      | Case (_,_,c,_) -> hrec c
+      | Case (_,_,_,c,_) -> hrec c
       | App (c,_)      -> hrec c
       | Cast (c,_,_)   -> hrec c
       | Proj (p, c)    -> hrec c
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index 553eb903fa..0f76fdda79 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -315,7 +315,7 @@ struct
           meta
       in
       Meta meta
-    | Case (ci,c1,c2,ca)     ->
+    | Case (ci,c1,_iv,c2,ca)     ->
       Term(DCase(ci,pat_of_constr c1,pat_of_constr c2,Array.map pat_of_constr ca))
     | Fix ((ia,i),(_,ta,ca)) ->
       Term(DFix(ia,i,Array.map pat_of_constr ta, Array.map pat_of_constr ca))