diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index e72580e696..3801a6fd88 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -627,7 +627,7 @@ let prim_refiner r sigma goal = check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let (sg,ev,sigma) = mk_goal sign cl' in - let ev = if k=VMcast then mkCast(ev,k,cl) else ev in + let ev = if k<>DEFAULTcast then mkCast(ev,k,cl) else ev in let sigma = Goal.V82.partial_solution sigma goal ev in ([sg], sigma) else |