Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.

1 files changed, 1 insertions, 1 deletions

diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 789028ac15..9580fdbfca 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -30,7 +30,7 @@ let absurd c =
     let sigma = Sigma.to_evar_map sigma in
     let j = Retyping.get_judgment_of env sigma (EConstr.of_constr c) in
     let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
-    let t = j.Environ.utj_val in
+    let t = EConstr.Unsafe.to_constr j.Environ.utj_val in
     let tac =
     Tacticals.New.tclTHENLIST [
       elim_type (build_coq_False ());