diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index 24c5a1266d..1424618f00 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; diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli index aed5b58b7a..bc5fc3e100 100644 --- a/plugins/subtac/subtac_obligations.mli +++ b/plugins/subtac/subtac_obligations.mli @@ -30,7 +30,7 @@ val add_definition : Names.identifier -> ?term:Term.constr -> Term.types -> ?reduce:(Term.constr -> Term.constr) -> ?hook:(Tacexpr.declaration_hook) -> obligation_info -> progress -type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option) list +type notations = (Vernacexpr.lstring * Topconstr.constr_expr * Topconstr.scope_name option) list type fixpoint_kind = | IsFixpoint of (identifier located option * Topconstr.recursion_order_expr) list |