Fix issue #354: support for defining values in SProp

src/covering.ml

@@ -670,11 +670,12 @@ let compute_fixdecls_data env evd ?data programs =
   in
   let fixprots =
     List.map (fun ty ->
-        let fixproto = get_efresh coq_fix_proto evd in
-        mkLetIn (anonR, fixproto,
+      let relevance = Retyping.relevance_of_type env !evd ty in
+      let fixproto = get_efresh coq_fix_proto evd in
+        relevance, mkLetIn (anonR, fixproto,
                  Retyping.get_type_of env !evd fixproto, ty)) tys in
   let fixdecls =
-    List.map2 (fun i fixprot -> of_tuple (nameR i, None, fixprot)) names fixprots in
+    List.map2 (fun i (relevance, fixprot) -> of_tuple (make_annot (Name i) relevance, None, fixprot)) names fixprots in
   data, List.rev fixdecls, fixprots
 
 let interp_arity env evd ~poly ~is_rec ~with_evars notations (((loc,i),rec_annot,l,t,by),clauses as ieqs) =

src/covering.mli

@@ -204,7 +204,7 @@ val compute_fixdecls_data :
            ?data:Constrintern.internalization_env ->
            Syntax.program_info list ->
            Constrintern.internalization_env *
-           Equations_common.rel_declaration list * EConstr.t list
+           Equations_common.rel_declaration list * (Sorts.relevance * EConstr.t) list
 
 val wf_fix_constr :
   Environ.env ->

src/depelim.ml

@@ -128,6 +128,8 @@ let annot_of_context ctx =
 let depcase ~poly (mind, i as ind) =
   let indid = Nametab.basename_of_global (GlobRef.IndRef ind) in
   let mindb, oneind = Global.lookup_inductive ind in
+  let relevance = oneind.mind_relevance in
+  let annotR x = make_annot x relevance in
   let inds = List.rev (Array.to_list (Array.mapi (fun i oib -> mkInd (mind, i)) mindb.mind_packets)) in
   let ctx = oneind.mind_arity_ctxt in
   let nparams = mindb.mind_nparams in
@@ -164,19 +166,13 @@ let depcase ~poly (mind, i as ind) =
         (make_assum (nameR (Id.of_string ("P" ^ string_of_int i))) br))
       oneind.mind_consnames oneind.mind_nf_lc
   in
-  let ci = make_case_info (Global.env ()) ind Sorts.Relevant RegularStyle in
-  (*   ci_ind = ind; *)
-  (*   ci_npar = nparams; *)
-  (*   ci_cstr_nargs = oneind.mind_consnrealargs; *)
-  (*   ci_cstr_ndecls = oneind.mind_consnrealdecls; *)
-  (*   ci_pp_info = { ind_tags = []; cstr_tags = [||]; style = RegularStyle; } } *)
-  (* in *)
+  let ci = make_case_info (Global.env ()) ind relevance RegularStyle in
   let obj i =
     mkApp (mkInd ind,
           (Array.append (extended_rel_vect (nargs + nconstrs + i) params)
               (extended_rel_vect 0 args)))
   in
-  let ctxpred = make_assum anonR (obj (2 + nargs)) :: args in
+  let ctxpred = make_assum (annotR Anonymous) (obj (2 + nargs)) :: args in
   let app = mkApp (mkRel (nargs + nconstrs + 3),
                   (extended_rel_vect 0 ctxpred))
   in

src/equations.ml

@@ -174,11 +174,12 @@ let define_by_eqs ~pm ~poly ~program_mode ~open_proof opts eqs nt =
                           program_split_info = info } in
     progs.(i) <- Some (p, compiled_info);
     if CArray.for_all (fun x -> not (Option.is_empty x)) progs then
-      (let fixprots = List.map (nf_evar !evd) fixprots in
+      (let fixprots = List.map (fun (rel, x) -> (rel, nf_evar !evd x)) fixprots in
        let progs = Array.map_to_list (fun x -> Option.get x) progs in
+       let relevant = List.for_all (fun (rel, x) -> rel == Sorts.Relevant) fixprots in
        let rec_info = compute_rec_type [] (List.map (fun (x, y) -> x.program_info) progs) in
        List.iter (Metasyntax.add_notation_interpretation (Global.env ())) nt;
-       if flags.with_eqns || flags.with_ind then
+       if (flags.with_eqns || flags.with_ind) && relevant then
          define_principles ~pm flags rec_info fixprots progs
        else pm)
     else pm

src/splitting.ml

@@ -519,6 +519,7 @@ let term_of_tree env0 isevar sort tree =
       let evm, block = Equations_common.(get_fresh evm coq_block) in
       let blockty = mkLetIn (anonR, block, Retyping.get_type_of env evm block, lift 1 ty) in
       let evd = ref evm in
+      let elim_relevance = Retyping.relevance_of_type (push_rel_context ctx env) evm ty in
       let ctx', case_ty, branches_res, nb_cuts, rev_subst, to_apply, simpl =
         Sigma_types.smart_case env evd ctx rel blockty in
 
@@ -629,7 +630,7 @@ let term_of_tree env0 isevar sort tree =
       let pind, args = find_inductive env !evd rel_ty in
 
       (* Build the case. *)
-      let case_info = Inductiveops.make_case_info env (fst pind) Sorts.Relevant Constr.RegularStyle in
+      let case_info = Inductiveops.make_case_info env (fst pind) elim_relevance Constr.RegularStyle in
       let indty = Inductiveops.find_rectype env !evd (mkApp (mkIndU pind, Array.map_of_list EConstr.of_constr args)) in
       let case = Inductiveops.make_case_or_project env !evd indty case_info
           case_ty rel_t branches in

test-suite/issues/issue354.v

@@ -0,0 +1,11 @@
+(* From Coq Require Import Logic.StrictProp. *)
+From Equations Require Import Equations.
+
+Inductive Ssig {A : Type} (P : A -> SProp) :=
+  | Sexists (a : A) (b : P a) : Ssig P.
+
+Equations Spr1 {A : Type} {P : A -> SProp} (s : Ssig P) : A :=
+  Spr1 (Sexists _ a b) := a.
+
+Equations Spr2 {A : Type} {P : A -> SProp} (s : Ssig P) : P (Spr1 s) :=
+  Spr2 (Sexists _ a b) := b.