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)

1 files changed, 1 insertions, 0 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59de85901..dc8f31859 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