summaryrefslogtreecommitdiff
path: root/contrib/subtac/subtac_interp_fixpoint.mli
blob: 149e7580795eaf9ce62298b017b0899c4854a953 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
val mkAppExplC :
  Libnames.reference * Topconstr.constr_expr list -> Topconstr.constr_expr
val mkSubset :
  Names.name Util.located ->
  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
val mkProj1 :
  Topconstr.constr_expr ->
  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
val mkProj2 :
  Topconstr.constr_expr ->
  Topconstr.constr_expr -> Topconstr.constr_expr -> Topconstr.constr_expr
val list_of_local_binders :
  Topconstr.local_binder list ->
  (Names.name Util.located * Topconstr.constr_expr) list
val pr_binder_list :
  (('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
val rewrite_rec_calls : 'a -> 'b -> 'b