Add relevance marks on binders.

Kernel should be mostly correct, higher levels do random stuff at
times.

1 files changed, 8 insertions, 6 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index bd95a62532..3ff2e3852d 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 open Constr
+open Context
 open EConstr
 open Hipattern
 open Tactics
@@ -19,10 +20,10 @@ module NamedDecl = Context.Named.Declaration
 
 (* Absurd *)
 
-let mk_absurd_proof coq_not t =
+let mk_absurd_proof coq_not r t =
   let id = Namegen.default_dependent_ident in
-  mkLambda (Names.Name id,mkApp(coq_not,[|t|]),
-    mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
+  mkLambda (make_annot (Names.Name id) Sorts.Relevant,mkApp(coq_not,[|t|]),
+    mkLambda (make_annot (Names.Name id) r,t,mkApp (mkRel 2,[|mkRel 1|])))
 
 let absurd c =
   Proofview.Goal.enter begin fun gl ->
@@ -31,12 +32,13 @@ let absurd c =
     let j = Retyping.get_judgment_of env sigma c in
     let sigma, j = Coercion.inh_coerce_to_sort env sigma j in
     let t = j.Environ.utj_val in
+    let r = Sorts.relevance_of_sort j.Environ.utj_type in
     Proofview.Unsafe.tclEVARS sigma <*>
     Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.not.type")) >>= fun coqnot ->
     Tacticals.New.pf_constr_of_global (Coqlib.(lib_ref "core.False.type")) >>= fun coqfalse ->
     Tacticals.New.tclTHENLIST [
       elim_type coqfalse;
-      Simple.apply (mk_absurd_proof coqnot t)
+      Simple.apply (mk_absurd_proof coqnot r t)
     ]
   end
 
@@ -68,9 +70,9 @@ let contradiction_context =
 	  if is_empty_type sigma typ then
 	    simplest_elim (mkVar id)
 	  else match EConstr.kind sigma typ with
-	  | Prod (na,t,u) when is_empty_type sigma u ->
+          | Prod (na,t,u) when is_empty_type sigma u ->
              let is_unit_or_eq = match_with_unit_or_eq_type sigma t in
-	     Tacticals.New.tclORELSE
+             Tacticals.New.tclORELSE
                (match is_unit_or_eq with
                | Some _ ->
                    let hd,args = decompose_app sigma t in