diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-12 01:52:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:48 +0100 |
| commit | 771be16883c8c47828f278ce49545716918764c4 (patch) | |
| tree | f3c0427596d447677c54c23455fcfbe7e3337b49 /tactics/contradiction.ml | |
| parent | 45562afa065aadc207dca4e904e309d835cb66ef (diff) | |
Hipattern 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 2058b95a6..a8be704b2 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 (EConstr.of_constr typ) in - if is_empty_type sigma typ then + if is_empty_type sigma (EConstr.of_constr typ) then simplest_elim (mkVar id) else match kind_of_term typ with - | Prod (na,t,u) when is_empty_type sigma u -> + | Prod (na,t,u) when is_empty_type sigma (EConstr.of_constr u) -> let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma (EConstr.of_constr 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 sigma u && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr t) + is_empty_type sigma (EConstr.of_constr u) && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr 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 (EConstr.of_constr c) in let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in - if is_empty_type sigma ccl then + if is_empty_type sigma (EConstr.of_constr ccl) then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) |