diff options
Diffstat (limited to 'plugins/subtac/subtac_obligations.ml')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 24c5a1266..1424618f0 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -49,7 +49,7 @@ type fixpoint_kind = | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list | IsCoFixpoint -type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list +type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list type program_info = { prg_name: identifier; |