Exploration towards including #311 in Coq#316

Draft

nomeata wants to merge 8 commits intodfinity:masterfrom

nomeata:joachim/coq-spec-variant

Commits on Jan 12, 2022

spec: subtype checking only for reference types
chenyan-dfinity
committed

Commits on Jan 13, 2022

Commits on Jan 14, 2022

Merge branch 'master' into spec-variant
chenyan-dfinity
authored

Commits on Feb 10, 2022

Exploration towards including #311 in Coq
nomeata
committed

Commits on Feb 19, 2022

Some more experiments, but still not good
nomeata
committed

Commits on Apr 7, 2022

Introduce type environment for refs; a bit of progress
nomeata
committed