From d5fece25d8964d5d9fcd55b66164286aeef5fb9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 14 Aug 2014 20:44:03 +0200
Subject: Reorganization of tactics: - made "apply" tactics of type
 Proofview.tactic, as well as other inner   functions about elim and assert -
 used same hypothesis naming policy for intros and internal_cut (towards a  
 reorganization of intro patterns) - "apply ... in H as pat" now supports any
 kind of introduction   pattern (doc not changed)

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

(limited to 'proofs')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59de859019..dc8f318598 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -573,6 +573,7 @@ let prim_refiner r sigma goal =
 	       raise (RefinerError IntroNeedsProduct))
 
     | Cut (b,replace,id,t) ->
+(*        if !check && not (Retyping.get_sort_of env sigma t) then*)
         let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
 	let sign,t,cl,sigma =
 	  if replace then
-- 
cgit v1.2.3