From 479d4cd6e9934a47debf6201fccf7ebb1aea1b09 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 7 Nov 2015 22:21:10 +0100
Subject: Implementing assert and cut with LetIn rather than using a
 beta-redex. Hopefully, it will provide with nicer proof terms, in combination
 with the commit printing the type of LetIn when the defined term is a proof.

---
 proofs/logic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index a38a36bdcc..e80f5a64c7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -532,7 +532,7 @@ let prim_refiner r sigma goal =
 	     push_named_context_val (id,None,t) sign,t,cl,sigma) in
         let (sg2,ev2,sigma) = 
 	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkApp (mkNamedLambda id t ev2 , [| ev1 |]) in
+	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
-- 
cgit v1.2.3