diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 16:18:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:44 +0100 |
| commit | b4b90c5d2e8c413e1981c456c933f35679386f09 (patch) | |
| tree | fc84ec244390beb2f495b024620af2e130ad5852 /tactics/contradiction.ml | |
| parent | 78a8d59b39dfcb07b94721fdcfd9241d404905d2 (diff) | |
Definining EConstr-based contexts.
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
Diffstat (limited to 'tactics/contradiction.ml')
| -rw-r--r-- | tactics/contradiction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 7173fb4fd..0e28aa980 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -51,7 +51,7 @@ let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 let filter_hyp f tac = let rec seek = function | [] -> Proofview.tclZERO Not_found - | d::rest when f (EConstr.of_constr (NamedDecl.get_type d)) -> tac (NamedDecl.get_id d) + | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter { enter = begin fun gl -> let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in @@ -66,7 +66,7 @@ let contradiction_context = | [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction") | d :: rest -> let id = NamedDecl.get_id d in - let typ = nf_evar sigma (EConstr.of_constr (NamedDecl.get_type d)) in + let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma typ in if is_empty_type sigma typ then simplest_elim (mkVar id) |