diff options
| author | Gaëtan Gilbert | 2020-05-07 16:01:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-07 16:01:03 +0200 |
| commit | e4bfbdfc4b4944d6e6d702eb732bce24f962e67f (patch) | |
| tree | 4a5ae5e1f3831c0a17c66cc7fc33de6721ec3a25 /vernac/comProgramFixpoint.mli | |
| parent | 17e7aeef98ca8c341fae05d5e94b50b4ee7687f6 (diff) | |
| parent | 223d0ad62896ce3a8831488acec133561cc9244b (diff) | |
Merge PR #12236: [funind] Remove use of low-level entries in scheme generation.
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'vernac/comProgramFixpoint.mli')
0 files changed, 0 insertions, 0 deletions