diff options
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index b9704b846..789028ac1 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -28,7 +28,7 @@ let absurd c = let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let sigma = Sigma.to_evar_map sigma in - let j = Retyping.get_judgment_of env sigma c in + let j = Retyping.get_judgment_of env sigma (EConstr.of_constr c) in let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in let t = j.Environ.utj_val in let tac = |