diff options
| author | Son Ho | 2023-06-02 00:18:23 +0200 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | 907fa4aefe4770d351b38a7f9a7a273030abf4c6 (patch) | |
| tree | ba26444e09a0e6c3465a9216bbaa68e336340f96 /compiler | |
| parent | efb0cd6eafbb25a51bba64ac613d910dcec4cfe7 (diff) | |
Use dune 3.7 and update the flake.lock
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/InterpreterLoopsMatchCtxs.mli | 6 | ||||
| -rw-r--r-- | compiler/aeneas.opam | 2 | ||||
| -rw-r--r-- | compiler/dune-project | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/compiler/InterpreterLoopsMatchCtxs.mli b/compiler/InterpreterLoopsMatchCtxs.mli index 7e585dd6..d0f57f32 100644 --- a/compiler/InterpreterLoopsMatchCtxs.mli +++ b/compiler/InterpreterLoopsMatchCtxs.mli @@ -42,7 +42,7 @@ val compute_abs_borrows_loans_maps : variant for instance) it calls the corresponding specialized function from {!InterpreterLoopsCore.PrimMatcher}. *) -module MakeMatcher : functor (PM : PrimMatcher) -> Matcher +module MakeMatcher : functor (_ : PrimMatcher) -> Matcher (** A matcher for joins (we use joins to compute loop fixed points). @@ -58,7 +58,7 @@ module MakeMatcher : functor (PM : PrimMatcher) -> Matcher The join matcher is used to match the *concrete* values only. For this reason, we fail on the functions which match avalues. *) -module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher +module MakeJoinMatcher : functor (_ : MatchJoinState) -> PrimMatcher (** An auxiliary matcher that we use for two purposes: - to check if two contexts are equivalent modulo id substitution (i.e., @@ -67,7 +67,7 @@ module MakeJoinMatcher : functor (S : MatchJoinState) -> PrimMatcher target context to the values and borrows in a source context (see {!match_ctx_with_target}). *) -module MakeCheckEquivMatcher : functor (S : MatchCheckEquivState) -> +module MakeCheckEquivMatcher : functor (_ : MatchCheckEquivState) -> CheckEquivMatcher (** Compute whether two contexts are equivalent modulo an identifier substitution. diff --git a/compiler/aeneas.opam b/compiler/aeneas.opam index 571b2d33..c92e8a1c 100644 --- a/compiler/aeneas.opam +++ b/compiler/aeneas.opam @@ -9,7 +9,7 @@ license: "Apache-2.0" homepage: "https://github.com/AeneasVerif/aeneas" bug-reports: "https://github.com/AeneasVerif/aeneas/issues" depends: [ - "dune" {>= "2.8"} + "dune" {>= "3.7"} "odoc" {with-doc} ] build: [ diff --git a/compiler/dune-project b/compiler/dune-project index 650eeec0..9910e549 100644 --- a/compiler/dune-project +++ b/compiler/dune-project @@ -1,4 +1,4 @@ -(lang dune 2.8) +(lang dune 3.7) (name aeneas) |