- | C.Variable (s, None, u, pars, attrs) ->
- out "Local declaration"
- | C.Variable (s, Some t, u, pars, attrs) ->
- out "Local definition"
- | C.CurrentProof (s, e, t, u, pars, attrs) ->
+ | C.Variable (s, None, u, pars, attrs) ->
+ out "local fun "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " of "; pp_term out [] [] u
+ | C.Variable (s, Some t, u, pars, attrs) ->
+ out "local let "; pp_attrs out attrs; out s; pp_pars out pars;
+ out " def "; pp_term out [] [] t; out " of "; pp_term out [] [] u
+ | C.InductiveDefinition (us, pars, lpsno, attrs) ->
+ out "Inductive "; pp_attrs out attrs; pp_int out lpsno; pp_pars out pars;
+ xiter out "" "\n" "" (pp_definition out) us
+ | C.CurrentProof (s, e, t, u, pars, attrs) ->