diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-10-30 17:53:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:20:30 +0100 |
| commit | 5143129baac805d3a49ac3ee9f3344c7a447634f (patch) | |
| tree | 60fd3fb22fc95474454a6a60f3a8715bf7d766d0 /tactics/contradiction.ml | |
| parent | a42795cc1c2a8ed3efa9960af920ff7b16d928f0 (diff) | |
Termops API using EConstr.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 6b29f574c..fcbad4bf0 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,12 +66,12 @@ let contradiction_context = let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in - if is_empty_type typ then + if is_empty_type sigma typ then simplest_elim (mkVar id) else match kind_of_term typ with - | Prod (na,t,u) when is_empty_type u -> + | Prod (na,t,u) when is_empty_type sigma u -> let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t else None in Tacticals.New.tclORELSE (match is_unit_or_eq with @@ -105,7 +105,7 @@ let is_negation_of env sigma typ t = match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in - is_empty_type u && is_conv_leq env sigma typ t + is_empty_type sigma u && is_conv_leq env sigma typ t | _ -> false let contradiction_term (c,lbind as cl) = @@ -115,7 +115,7 @@ let contradiction_term (c,lbind as cl) = let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of c in let _, ccl = splay_prod env sigma typ in - if is_empty_type ccl then + if is_empty_type sigma ccl then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) |