diff options
| author | Pierre-Marie Pédrot | 2016-03-06 03:02:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-06 03:25:30 +0100 |
| commit | 8d828a124d66a79b6e35c02097b05df252d1e1d4 (patch) | |
| tree | a86a185c64e9e998eb871e37f50ec3030250d1d6 /plugins | |
| parent | f8b624f7bec0406258eee4e08b0cec8d756da6ff (diff) | |
Moving Eauto to a simple ML file.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index c8f8a19e5b..02cd819f4a 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = (* let ids = List.filter (fun id -> not (List.mem id ids)) ids' in *) (* rewrite *) (* ) *) - Eauto.gen_eauto (false,5) [] (Some []) + Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some [])) ] gls |