diff options
Diffstat (limited to 'src/tac2quote.ml')
| -rw-r--r-- | src/tac2quote.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/tac2quote.ml b/src/tac2quote.ml index f14612d58f..a5c5c7d31f 100644 --- a/src/tac2quote.ml +++ b/src/tac2quote.ml @@ -370,3 +370,13 @@ let of_move_location (loc, mv) = match mv with | QMoveBefore id -> std_constructor ?loc "MoveBefore" [of_anti of_ident id] | QMoveFirst -> std_constructor ?loc "MoveFirst" [] | QMoveLast -> std_constructor ?loc "MoveLast" [] + +let of_generalization (loc, (c, occ, na)) = + of_tuple ?loc [ + of_open_constr c; + of_occurrences occ; + of_option (fun id -> of_anti of_ident id) na; + ] + +let of_generalizations (loc, l) = + of_list ?loc of_generalization l |