Skip to content

Commit

Permalink
Require new Ltac2 files in [Ltac2.v].
Browse files Browse the repository at this point in the history
  • Loading branch information
Rodolphe Lepigre committed Oct 13, 2023
1 parent 2176920 commit 9dd3091
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions user-contrib/Ltac2/Ltac2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,7 @@ Require Ltac2.Fresh.
Require Ltac2.Ident.
Require Ltac2.Ind.
Require Ltac2.Int.
Require Ltac2.Lazy.
Require Ltac2.List.
Require Ltac2.Ltac1.
Require Ltac2.Message.
Expand All @@ -32,6 +33,8 @@ Require Ltac2.Option.
Require Ltac2.Pattern.
Require Ltac2.Printf.
Require Ltac2.Proj.
Require Ltac2.RedFlags.
Require Ltac2.Ref.
Require Ltac2.Std.
Require Ltac2.String.
Require Ltac2.Uint63.
Expand Down

0 comments on commit 9dd3091

Please sign in to comment.