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.

6 files changed, 17 insertions, 11 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0a5f1ba68..095521e25 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -75,6 +75,8 @@ type constr = t
 type existential = t pexistential
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
+type unsafe_judgment = (constr, types) Environ.punsafe_judgment
+type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
 let mkProp = of_kind (Sort Sorts.prop)
 let mkSet = of_kind (Sort Sorts.set)
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 03e2d4ffc..10eb064a3 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -20,6 +20,8 @@ type constr = t
 type existential = t pexistential
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
+type unsafe_judgment = (constr, types) Environ.punsafe_judgment
+type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
 (** {5 Destructors} *)
 
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index fc193b94a..bc55ac458 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -96,14 +96,15 @@ let rec whd_evar sigma c =
     | _ -> c
 
 let rec nf_evar sigma t = Constr.map (fun t -> nf_evar sigma t) (whd_evar sigma t)
+let e_nf_evar sigma t = EConstr.of_constr (nf_evar sigma (EConstr.Unsafe.to_constr t))
 
 let j_nf_evar sigma j =
-  { uj_val = nf_evar sigma j.uj_val;
-    uj_type = nf_evar sigma j.uj_type }
+  { uj_val = e_nf_evar sigma j.uj_val;
+    uj_type = e_nf_evar sigma j.uj_type }
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=nf_evar sigma v;utj_type=t}
+  {utj_val=e_nf_evar sigma v;utj_type=t}
 
 let nf_evars_universes evm =
   Universes.nf_evars_and_universes_opt_subst (safe_evar_value evm) 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index dcb9bf247..8f3c3c352 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -141,13 +141,13 @@ val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 
 val whd_evar :  evar_map -> constr -> constr
 val nf_evar :  evar_map -> constr -> constr
-val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment
+val j_nf_evar :  evar_map -> EConstr.unsafe_judgment -> EConstr.unsafe_judgment
 val jl_nf_evar :
-   evar_map -> unsafe_judgment list -> unsafe_judgment list
+   evar_map -> EConstr.unsafe_judgment list -> EConstr.unsafe_judgment list
 val jv_nf_evar :
-   evar_map -> unsafe_judgment array -> unsafe_judgment array
+   evar_map -> EConstr.unsafe_judgment array -> EConstr.unsafe_judgment array
 val tj_nf_evar :
-   evar_map -> unsafe_type_judgment -> unsafe_type_judgment
+   evar_map -> EConstr.unsafe_type_judgment -> EConstr.unsafe_type_judgment
 
 val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
 val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
diff --git a/engine/termops.ml b/engine/termops.ml
index c1198e05a..83f07d2c6 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1141,6 +1141,7 @@ let impossible_default_case = ref None
 let set_impossible_default_clause c = impossible_default_case := Some c
 
 let coq_unit_judge =
+  let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
   let na1 = Name (Id.of_string "A") in
   let na2 = Name (Id.of_string "H") in
   fun () ->
diff --git a/engine/termops.mli b/engine/termops.mli
index df3fdd124..27b3ea53c 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -274,10 +274,10 @@ val is_template_polymorphic : env -> Evd.evar_map -> EConstr.t -> bool
 
 (** Combinators on judgments *)
 
-val on_judgment       : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_value : (types -> types) -> unsafe_judgment -> unsafe_judgment
-val on_judgment_type  : (types -> types) -> unsafe_judgment -> unsafe_judgment
+val on_judgment       : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment
+val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
+val on_judgment_type  : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment
 
 (** {6 Functions to deal with impossible cases } *)
 val set_impossible_default_clause : (unit -> (constr * types) Univ.in_universe_context_set) -> unit
-val coq_unit_judge : unit -> unsafe_judgment Univ.in_universe_context_set
+val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set