diff options
| author | Pierre-Marie Pédrot | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /plugins/funind/functional_principles_proofs.ml | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'plugins/funind/functional_principles_proofs.ml')
| -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 0a7938069f..83fc48623c 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -1150,7 +1150,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam let info_array = Array.mapi (fun i types -> - let types = prod_applist types (List.rev_map var_of_decl princ_params) in + let types = Term.prod_applist types (List.rev_map var_of_decl princ_params) in { idx = idxs.(i) - fix_offset; name = Nameops.out_name (fresh_id names.(i)); types = types; |