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.
---
 ltac/tacinterp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index d8c9339121..142f061b5a 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -2100,11 +2100,13 @@ let interp_redexp env sigma r =
 
 let _ =
   let eval ty env sigma lfun arg =
+    let ty = EConstr.Unsafe.to_constr ty in
     let ist = { lfun = lfun; extra = TacStore.empty; } in
     if Genarg.has_type arg (glbwit wit_tactic) then
       let tac = Genarg.out_gen (glbwit wit_tactic) arg in
       let tac = interp_tactic ist tac in
-      Pfedit.refine_by_tactic env sigma ty tac
+      let (c, sigma) = Pfedit.refine_by_tactic env sigma ty tac in
+      (EConstr.of_constr c, sigma)
     else
       failwith "not a tactic"
   in
-- 
cgit v1.2.3