diff options
Diffstat (limited to 'contrib/interface/xlate.ml')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index f17cb67b4..323d885a2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1161,8 +1161,8 @@ and xlate_tac = (xlate_int_or_constr a, xlate_using b, xlate_with_names c) | TacNewInduction(a,b,c) -> - CT_new_induction - (xlate_int_or_constr a, xlate_using b, + CT_new_induction (* Pierre C. : est-ce correct *) + (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, |