diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 21:54:11 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-28 21:54:11 +0200 |
| commit | f5e0757c1df43f315a425b8fe4d3397818f8cb76 (patch) | |
| tree | aea1f671a7486d7449ad6883f08e6e9a2ce4f744 /plugins/funind/invfun.ml | |
| parent | fe62902764cc52daa985ad03e6f7ac0f8f1c2c4c (diff) | |
| parent | 5cc13770ac2358d583b21f217b8c65d2d5abd850 (diff) | |
Merge PR#678: [coqlib] Move `Coqlib` to `library/`.
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8c972cd7c..8eaa9b0f5 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -546,7 +546,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ |