diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-21 12:13:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd (patch) | |
| tree | 101bd3bc2e05eb52bfc142587d425f8920671b25 /tactics/contradiction.ml | |
| parent | e09f3b44bb381854b647a6d9debdeddbfc49177e (diff) | |
Reductionops now return EConstrs.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 2d5c28eba..afc7e1547 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -69,7 +69,6 @@ let contradiction_context = let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = EConstr.of_constr typ in let typ = whd_all env sigma typ in - let typ = EConstr.of_constr typ in if is_empty_type sigma typ then simplest_elim (mkVar id) else match EConstr.kind sigma typ with @@ -106,7 +105,7 @@ let contradiction_context = end } let is_negation_of env sigma typ t = - match EConstr.kind sigma (EConstr.of_constr (whd_all env sigma t)) with + match EConstr.kind sigma (whd_all env sigma t) with | Prod (na,t,u) -> is_empty_type sigma u && is_conv_leq env sigma typ t | _ -> false |