diff options
| author | coqbot-app[bot] | 2020-11-26 11:06:00 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-26 11:06:00 +0000 |
| commit | 0fc82e9651ee1dbc429c9b328b90ad8ad1a3cb14 (patch) | |
| tree | c99091031ad585bf3249ae089e12f44d4e5d83ce /lib | |
| parent | 5c7f71a270b265d1ae3f86cb2a29d28f2310edc5 (diff) | |
| parent | 4011a9137fdebe16aa40cb03ba5ce32c09687c69 (diff) | |
Merge PR #13415: Separate interning and pretyping of universes
Reviewed-by: mattam82
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cAst.ml | 2 | ||||
| -rw-r--r-- | lib/cAst.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/lib/cAst.ml b/lib/cAst.ml index 18fa1c9b0d..30b7fca587 100644 --- a/lib/cAst.ml +++ b/lib/cAst.ml @@ -24,3 +24,5 @@ let map_from_loc f l = let with_val f n = f n.v let with_loc_val f n = f ?loc:n.loc n.v + +let eq f x y = f x.v y.v diff --git a/lib/cAst.mli b/lib/cAst.mli index 2e07d1cd78..025bdf25ab 100644 --- a/lib/cAst.mli +++ b/lib/cAst.mli @@ -22,3 +22,5 @@ val map_from_loc : (?loc:Loc.t -> 'a -> 'b) -> 'a Loc.located -> 'b t val with_val : ('a -> 'b) -> 'a t -> 'b val with_loc_val : (?loc:Loc.t -> 'a -> 'b) -> 'a t -> 'b + +val eq : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool |