Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

7 files changed, 49 insertions, 40 deletions

diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index b0277e9cc2..050fdcb608 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -11,6 +11,7 @@
 open Util
 open Names
 open Constr
+open Context
 open CErrors
 open Evar_refiner
 open Tacmach
@@ -62,7 +63,7 @@ let instantiate_tac n c ido =
 		  evar_list sigma (EConstr.of_constr (NamedDecl.get_type decl))
 	      | InHypValueOnly ->
 		  (match decl with
-		    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
+                    | LocalDef (_,body,_) -> evar_list sigma (EConstr.of_constr body)
 		    | _ -> user_err Pp.(str "Not a defined hypothesis.")) in
   if List.length evl < n then
     user_err Pp.(str "Not enough uninstantiated existential variables.");
@@ -108,5 +109,6 @@ let hget_evar n =
   if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
   let ev = List.nth evl (n-1) in
   let ev_type = EConstr.existential_type sigma ev in
-  Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl))
+  let r = Retyping.relevance_of_type (Proofview.Goal.env gl) sigma ev_type in
+  Tactics.change_concl (mkLetIn (make_annot Name.Anonymous r,mkEvar ev,ev_type,concl))
   end
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index ffd8b71e5d..0428f08138 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -12,6 +12,7 @@
 
 open Pp
 open Constr
+open Context
 open Genarg
 open Stdarg
 open Tacarg
@@ -674,7 +675,7 @@ let hResolve id c occ t =
   let sigma = Evd.merge_universe_context sigma ctx in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
-    (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl)))
+    (change_concl (mkLetIn (make_annot Name.Anonymous Sorts.Relevant,t_constr,t_constr_type,concl)))
   end
 
 let hResolve_auto id c t =
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 5e3f4df192..e188971f00 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s =
       if n=0 then (List.rev acc, EConstr.of_constr ty) else
         match Constr.kind ty with
         | Constr.Prod(na,a,b) ->
-          strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b
+          strip_ty (([CAst.make na.Context.binder_name],EConstr.of_constr a)::acc) (n-1) b
         | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
     strip_ty [] n ty
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e78d0f93a4..b1d5c0252f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -15,6 +15,7 @@ open Names
 open Nameops
 open Namegen
 open Constr
+open Context
 open EConstr
 open Vars
 open Reduction
@@ -220,23 +221,23 @@ end) = struct
     let rec aux env evars ty l =
       let t = Reductionops.whd_all env (goalevars evars) ty in
 	match EConstr.kind (goalevars evars) t, l with
-	| Prod (na, ty, b), obj :: cstrs ->
+        | Prod (na, ty, b), obj :: cstrs ->
           let b = Reductionops.nf_betaiota env (goalevars evars) b in
-	  if noccurn (goalevars evars) 1 b (* non-dependent product *) then
+          if noccurn (goalevars evars) 1 b (* non-dependent product *) then
             let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
 	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
 	    let evars, relty = mk_relty evars env ty obj in
 	    let evars, newarg = app_poly env evars respectful [| ty ; b' ; relty ; arg |] in
-	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
+              evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
 	  else
 	    let (evars, b, arg, cstrs) =
-	      aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
+              aux (push_rel (LocalAssum (na, ty)) env) evars b cstrs
 	    in
             let ty = Reductionops.nf_betaiota env (goalevars evars) ty in
-	    let pred = mkLambda (na, ty, b) in
-	    let liftarg = mkLambda (na, ty, arg) in
-	    let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
-	      if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
+            let pred = mkLambda (na, ty, b) in
+            let liftarg = mkLambda (na, ty, arg) in
+            let evars, arg' = app_poly env evars forall_relation [| ty ; pred ; liftarg |] in
+              if Option.is_empty obj then evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	      else user_err Pp.(str "build_signature: no constraint can apply on a dependent argument")
 	| _, obj :: _ -> anomaly ~label:"build_signature" (Pp.str "not enough products.")
 	| _, [] ->
@@ -253,7 +254,7 @@ end) = struct
   let unfold_impl sigma t =
     match EConstr.kind sigma t with
     | App (arrow, [| a; b |])(*  when eq_constr arrow (Lazy.force impl) *) ->
-      mkProd (Anonymous, a, lift 1 b)
+      mkProd (make_annot Anonymous Sorts.Relevant, a, lift 1 b)
     | _ -> assert false
 
   let unfold_all sigma t =
@@ -279,7 +280,7 @@ end) = struct
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 	(* (evd, mkProd (Anonymous, a, b)), (fun x -> x) *)
       else if bp then (* Dummy forall *)
-	(app_poly env evd coq_all [| a; mkLambda (Anonymous, a, lift 1 b) |]), unfold_forall
+        (app_poly env evd coq_all [| a; mkLambda (make_annot Anonymous Sorts.Relevant, a, lift 1 b) |]), unfold_forall
       else (* None in Prop, use arrow *)
 	(app_poly env evd arrow [| a; b |]), unfold_impl
 
@@ -308,7 +309,8 @@ end) = struct
       app_poly env evd pointwise_relation [| t; lift (-1) car; lift (-1) rel |]
     else
       app_poly env evd forall_relation
-	[| t; mkLambda (n, t, car); mkLambda (n, t, rel) |]
+        [| t; mkLambda (make_annot n Sorts.Relevant, t, car);
+           mkLambda (make_annot n Sorts.Relevant, t, rel) |]
 
   let lift_cstr env evars (args : constr list) c ty cstr =
     let start evars env car =
@@ -323,15 +325,15 @@ end) = struct
       else
         let sigma = goalevars evars in
 	match EConstr.kind sigma (Reductionops.whd_all env sigma prod) with
-	| Prod (na, ty, b) ->
+        | Prod (na, ty, b) ->
 	  if noccurn sigma 1 b then
 	    let b' = lift (-1) b in
 	    let evars, rb = aux evars env b' (pred n) in
 	      app_poly env evars pointwise_relation [| ty; b'; rb |]
 	  else
-	    let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
+            let evars, rb = aux evars (push_rel (LocalAssum (na, ty)) env) b (pred n) in
 	      app_poly env evars forall_relation
-		[| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
+                [| ty; mkLambda (na, ty, b); mkLambda (na, ty, rb) |]
 	| _ -> raise Not_found
     in 
     let rec find env c ty = function
@@ -481,8 +483,9 @@ let rec decompose_app_rel env evd t =
   | App (f, [|arg|]) ->
     let (f', argl, argr) = decompose_app_rel env evd arg in
     let ty = Typing.unsafe_type_of env evd argl in
-    let f'' = mkLambda (Name default_dependent_ident, ty,
-      mkLambda (Name (Id.of_string "y"), lift 1 ty,
+    let r = Retyping.relevance_of_type env evd ty in
+    let f'' = mkLambda (make_annot (Name default_dependent_ident) r, ty,
+      mkLambda (make_annot (Name (Id.of_string "y")) r, lift 1 ty,
         mkApp (lift 2 f, [| mkApp (lift 2 f', [| mkRel 2; mkRel 1 |]) |])))
     in (f'', argl, argr)
   | App (f, args) ->
@@ -522,7 +525,7 @@ let decompose_applied_relation env sigma (c,l) =
     | Some c -> c
     | None ->
 	let ctx,t' = Reductionops.splay_prod env sigma ctype in (* Search for underlying eq *)
-	match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
+        match find_rel (it_mkProd_or_LetIn t' (List.map (fun (n,t) -> LocalAssum (n, t)) ctx)) with
 	| Some c -> c
 	| None -> user_err Pp.(str "Cannot find an homogeneous relation to rewrite.")
 
@@ -803,7 +806,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
 	else TypeGlobal.do_subrelation, TypeGlobal.apply_subrelation
       in
 	EConstr.push_named
-	  (LocalDef (Id.of_string "do_subrelation",
+          (LocalDef (make_annot (Id.of_string "do_subrelation") Sorts.Relevant,
 	             snd (app_poly_sort b env evars dosub [||]),
 	             snd (app_poly_nocheck env evars appsub [||])))
 	  env
@@ -906,7 +909,7 @@ let make_leibniz_proof env c ty r =
 	let prf =
 	  e_app_poly env evars coq_f_equal
 		[| r.rew_car; ty;
-		   mkLambda (Anonymous, r.rew_car, c);
+                   mkLambda (make_annot Anonymous Sorts.Relevant, r.rew_car, c);
 		   r.rew_from; r.rew_to; prf |]
 	in RewPrf (rel, prf)
     | RewCast k -> r.rew_prf
@@ -1103,7 +1106,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       (* 		else *)
 
       | Prod (n, dom, codom) ->
-	  let lam = mkLambda (n, dom, codom) in
+          let lam = mkLambda (n, dom, codom) in
 	  let (evars', app), unfold = 
 	    if eq_constr (fst evars) ty mkProp then
 	      (app_poly_sort prop env evars coq_all [| dom; lam |]), TypeGlobal.unfold_all
@@ -1149,9 +1152,9 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
       (* 	    | _ -> b') *)
 
       | Lambda (n, t, b) when flags.under_lambdas ->
-        let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in
+        let n' = map_annot (Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env)) n in
         let open Context.Rel.Declaration in
-	let env' = EConstr.push_rel (LocalAssum (n', t)) env in
+        let env' = EConstr.push_rel (LocalAssum (n', t)) env in
 	let bty = Retyping.get_type_of env' (goalevars evars) b in
 	let unlift = if prop then PropGlobal.unlift_cstr else TypeGlobal.unlift_cstr in
 	let state, b' = s.strategy { state ; env = env' ; unfresh ;
@@ -1166,15 +1169,15 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy =
 		let point = if prop then PropGlobal.pointwise_or_dep_relation else
 		    TypeGlobal.pointwise_or_dep_relation
 		in
-		let evars, rel = point env r.rew_evars n' t r.rew_car rel in
-		let prf = mkLambda (n', t, prf) in
+                let evars, rel = point env r.rew_evars n'.binder_name t r.rew_car rel in
+                let prf = mkLambda (n', t, prf) in
 		  { r with rew_prf = RewPrf (rel, prf); rew_evars = evars }
 	      | x -> r
 	    in
 	      Success { r with
-		rew_car = mkProd (n, t, r.rew_car);
-		rew_from = mkLambda(n, t, r.rew_from);
-		rew_to = mkLambda (n, t, r.rew_to) }
+                rew_car = mkProd (n, t, r.rew_car);
+                rew_from = mkLambda(n, t, r.rew_from);
+                rew_to = mkLambda (n, t, r.rew_to) }
 	  | Fail | Identity -> b'
 	in state, res
 	    
@@ -1516,7 +1519,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
 	    | Some (t, ty) ->
               let t = Reductionops.nf_evar evars' t in
               let ty = Reductionops.nf_evar evars' ty in
-		mkApp (mkLambda (Name (Id.of_string "lemma"), ty, p), [| t |])
+                mkApp (mkLambda (make_annot (Name (Id.of_string "lemma")) Sorts.Relevant, ty, p), [| t |])
 	  in
 	  let proof = match is_hyp with
             | None -> term
@@ -1542,7 +1545,8 @@ let assert_replacing id newt tac =
     let after, before = List.split_when (NamedDecl.get_id %> Id.equal id) ctx in
     let nc = match before with
     | [] -> assert false
-    | d :: rem -> insert_dependent env sigma (LocalAssum (NamedDecl.get_id d, newt)) [] after @ rem
+    | d :: rem -> insert_dependent env sigma
+                    (LocalAssum (make_annot (NamedDecl.get_id d) Sorts.Relevant, newt)) [] after @ rem
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Refine.refine ~typecheck:true begin fun sigma ->
@@ -1586,7 +1590,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
 	    tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id)
 	| Some id, None ->
             Proofview.Unsafe.tclEVARS undef <*>
-            convert_hyp_no_check (LocalAssum (id, newt)) <*>
+            convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*>
             beta_hyp id
 	| None, Some p ->
             Proofview.Unsafe.tclEVARS undef <*>
@@ -1905,7 +1909,7 @@ let build_morphism_signature env sigma m =
   let cstrs =
     let rec aux t =
       match EConstr.kind sigma t with
-	| Prod (na, a, b) ->
+        | Prod (na, a, b) ->
 	    None :: aux b
 	| _ -> []
     in aux t
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 026c00b849..fcab98c7e8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -199,7 +199,8 @@ let id_of_name = function
 	  basename
        | Sort s ->
           begin
-	    match ESorts.kind sigma s with
+            match ESorts.kind sigma s with
+            | Sorts.SProp -> Label.to_id (Label.make "SProp")
             | Sorts.Prop -> Label.to_id (Label.make "Prop")
             | Sorts.Set -> Label.to_id (Label.make "Set")
             | Sorts.Type _ -> Label.to_id (Label.make "Type")
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 54924f1644..2b5e496168 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -12,6 +12,7 @@
     (lazy)match and (lazy)match goal. *)
 
 open Names
+open Context
 open Tacexpr
 open Context.Named.Declaration
 
@@ -299,8 +300,8 @@ module PatternMatching (E:StaticEnvironment) = struct
       | LocalDef (id,body,hyp) ->
           pattern_match_term false bodypat body () <*>
           pattern_match_term true typepat hyp () <*>
-          put_terms (id_map_try_add_name hypname (EConstr.mkVar id) empty_term_subst) <*>
-          return id
+          put_terms (id_map_try_add_name hypname (EConstr.mkVar id.binder_name) empty_term_subst) <*>
+          return id.binder_name
       | LocalAssum (id,hyp) -> fail
 
   (** [hyp_match pat hyps] dispatches to
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 19256e054d..4c65445b89 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -142,7 +142,7 @@ let flatten_contravariant_conj _ ist =
           ~onlybinary:flags.binary_mode typ
   with
   | Some (_,args) ->
-    let newtyp = List.fold_right mkArrow args c in
+    let newtyp = List.fold_right (fun a b -> mkArrow a Sorts.Relevant b) args c in
     let intros = tclMAP (fun _ -> intro) args in
     let by = tclTHENLIST [intros; apply hyp; split; assumption] in
     tclTHENLIST [assert_ ~by newtyp; clear (destVar sigma hyp)]
@@ -173,7 +173,7 @@ let flatten_contravariant_disj _ ist =
           typ with
   | Some (_,args) ->
       let map i arg =
-        let typ = mkArrow arg c in
+        let typ = mkArrow arg Sorts.Relevant c in
         let ci = Tactics.constructor_tac false None (succ i) Tactypes.NoBindings in
         let by = tclTHENLIST [intro; apply hyp; ci; assumption] in
         assert_ ~by typ