diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 1 |
1 files changed, 1 insertions, 0 deletions
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 |