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

2 files changed, 19 insertions, 16 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 575d964158..23cdae7883 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -17,6 +17,7 @@ open Pp
 open Names
 open Sorts
 open Constr
+open Context
 open Vars
 open Goptions
 open Tacmach
@@ -421,11 +422,11 @@ let new_representative typ =
 
 let _A_ = Name (Id.of_string "A")
 let _B_ = Name (Id.of_string "A")
-let _body_ =  mkProd(Anonymous,mkRel 2,mkRel 2)
+let _body_ =  mkProd(make_annot Anonymous Sorts.Relevant,mkRel 2,mkRel 2)
 
 let cc_product s1 s2 =
-  mkLambda(_A_,mkSort(s1),
-	   mkLambda(_B_,mkSort(s2),_body_))
+  mkLambda(make_annot _A_ Sorts.Relevant,mkSort(s1),
+           mkLambda(make_annot _B_ Sorts.Relevant,mkSort(s2),_body_))
 
 let rec constr_of_term = function
     Symb s-> s
@@ -452,11 +453,11 @@ let rec canonize_name sigma c =
 	  let canon_mind = MutInd.make1 (MutInd.canonical kn) in
 	    mkConstructU (((canon_mind,i),j),u)
       | Prod (na,t,ct) ->
-	  mkProd (na,func t, func ct)
+          mkProd (na,func t, func ct)
       | Lambda (na,t,ct) ->
-	  mkLambda (na, func t,func ct)
+          mkLambda (na, func t,func ct)
       | LetIn (na,b,t,ct) ->
-	  mkLetIn (na, func b,func t,func ct)
+          mkLetIn (na, func b,func t,func ct)
       | App (ct,l) ->
           mkApp (func ct,Array.Smart.map func l)
       | Proj(p,c) ->
@@ -806,7 +807,8 @@ let __eps__ = Id.of_string "_eps_"
 let new_state_var typ state =
   let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
   let id = Namegen.next_ident_away __eps__ ids in
-  state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env;
+  let r = Sorts.Relevant in (* TODO relevance *)
+  state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env;
   id
 
 let complete_one_class state i=
@@ -814,9 +816,9 @@ let complete_one_class state i=
       Partial pac ->
 	let rec app t typ n =
 	  if n<=0 then t else
-	    let _,etyp,rest= destProd typ in
+            let _,etyp,rest= destProd typ in
             let id = new_state_var (EConstr.of_constr etyp) state in
-		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
+                app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
         let _c = Typing.unsafe_type_of state.env state.sigma
 	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
         let _c = EConstr.Unsafe.to_constr _c in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 055d36747d..5778acce0a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -15,6 +15,7 @@ open Names
 open Inductiveops
 open Declarations
 open Constr
+open Context
 open EConstr
 open Vars
 open Tactics
@@ -151,19 +152,19 @@ let patterns_of_constr env sigma nrels term=
 
 let rec quantified_atom_of_constr env sigma nrels term =
   match EConstr.kind sigma (whd_delta env sigma term) with
-      Prod (id,atom,ff) -> 
+      Prod (id,atom,ff) ->
 	if is_global sigma (Lazy.force _False) ff then
 	  let patts=patterns_of_constr env sigma nrels atom in
 	      `Nrule patts
 	else 
-	  quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
+          quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff
     | _ ->  
 	let patts=patterns_of_constr env sigma nrels term in
 	    `Rule patts
 
 let litteral_of_constr env sigma term=
   match EConstr.kind sigma (whd_delta env sigma term) with
-    | Prod (id,atom,ff) -> 
+    | Prod (id,atom,ff) ->
 	if is_global sigma (Lazy.force _False) ff then
 	  match (atom_of_constr env sigma atom) with
 	      `Eq(t,a,b) -> `Neq(t,a,b)
@@ -171,7 +172,7 @@ let litteral_of_constr env sigma term=
 	else
 	  begin
 	    try 
-	      quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
+              quantified_atom_of_constr (EConstr.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff
 	    with Not_found ->
 	      `Other (decompose_term env sigma term)
 	  end
@@ -233,7 +234,7 @@ let build_projection intype (cstr:pconstructor) special default gls=
   let sigma = project gls in
   let body=Equality.build_selector (pf_env gls) sigma ci (mkRel 1) intype special default in
   let id=pf_get_new_id (Id.of_string "t") gls in
-  sigma, mkLambda(Name id,intype,body)
+  sigma, mkLambda(make_annot (Name id) Sorts.Relevant,intype,body)
 
 (* generate an adhoc tactic following the proof tree  *)
 
@@ -318,7 +319,7 @@ let rec proof_tac p : unit Proofview.tactic =
 	refresh_universes (type_of tx1) (fun typx ->
 	refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx ->
         let id = Tacmach.New.pf_get_new_id (Id.of_string "f") gl in
-	let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in
+        let appx1 = mkLambda(make_annot (Name id) Sorts.Relevant,typf,mkApp(mkRel 1,[|tx1|])) in
 	let lemma1 = app_global_with_holes _f_equal [|typf;typfx;appx1;tf1;tf2|] 1 in
 	let lemma2 = app_global_with_holes _f_equal [|typx;typfx;tf2;tx1;tx2|] 1 in
 	let prf =
@@ -377,7 +378,7 @@ let convert_to_goal_tac c t1 t2 p =
     let neweq= app_global _eq [|sort;tt1;tt2|] in
     let e = Tacmach.New.pf_get_new_id (Id.of_string "e") gl in
     let x = Tacmach.New.pf_get_new_id (Id.of_string "X") gl in
-    let identity=mkLambda (Name x,sort,mkRel 1) in
+    let identity=mkLambda (make_annot (Name x) Sorts.Relevant,sort,mkRel 1) in
     let endt = app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in
     Tacticals.New.tclTHENS (neweq (assert_before (Name e)))
 			   [proof_tac p; endt refine_exact_check]