From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: 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.
---
 proofs/clenv.ml   | 6 ++++--
 proofs/refine.ml  | 5 ++++-
 proofs/refine.mli | 2 +-
 3 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 2d621e97cb..956be88c8a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -669,12 +669,14 @@ let evar_of_binder holes = function
     user_err  (str "No such binder.")
 
 let define_with_type sigma env ev c =
+  let c = EConstr.of_constr c in
   let t = Retyping.get_type_of env sigma (EConstr.of_constr ev) in
-  let ty = Retyping.get_type_of env sigma (EConstr.of_constr c) in
+  let ty = Retyping.get_type_of env sigma c in
+  let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j (EConstr.of_constr t) in
   let (ev, _) = destEvar ev in
-  let sigma = Evd.define ev j.Environ.uj_val sigma in
+  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 0ed74c9b36..067764c000 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -133,7 +133,9 @@ let refine ?(unsafe = true) f =
 (** Useful definitions *)
 
 let with_type env evd c t =
-  let my_type = Retyping.get_type_of env evd (EConstr.of_constr c) in
+  let c = EConstr.of_constr c in
+  let my_type = Retyping.get_type_of env evd c in
+  let my_type = EConstr.of_constr my_type in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
     Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j (EConstr.of_constr t)
@@ -147,6 +149,7 @@ let refine_casted ?unsafe f = Proofview.Goal.enter { enter = begin fun gl ->
   let f = { run = fun h ->
     let Sigma (c, h, p) = f.run h in
     let sigma, c = with_type env (Sigma.to_evar_map h) c concl in
+    let c = EConstr.Unsafe.to_constr c in
     Sigma (c, Sigma.Unsafe.of_evar_map sigma, p)
   } in
   refine ?unsafe f
diff --git a/proofs/refine.mli b/proofs/refine.mli
index 3d140f036b..4158e446cc 100644
--- a/proofs/refine.mli
+++ b/proofs/refine.mli
@@ -36,7 +36,7 @@ val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic
 (** {7 Helper functions} *)
 
 val with_type : Environ.env -> Evd.evar_map ->
-  Term.constr -> Term.types -> Evd.evar_map * Term.constr
+  Term.constr -> Term.types -> Evd.evar_map * EConstr.constr
 (** [with_type env sigma c t] ensures that [c] is of type [t]
     inserting a coercion if needed. *)
 
-- 
cgit v1.2.3