diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-11-22 13:21:31 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-05 10:01:21 +0100 |
| commit | e7f7fc3e0582867975642fcaa7bd42140c61cd99 (patch) | |
| tree | 4005a4e4c4608449722043346e95c111df1d7b68 /kernel/inductive.ml | |
| parent | ade2363e357db3ac3f258e645fe6bba988e7e7dd (diff) | |
Simplifying an instantiation function using subst_of_rel_context_instance.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions