search

snu-sf / CompCertM

6 stars 5 forks source link

Remove unwanted import #22

Open alxest opened 4 years ago

alxest commented 4 years ago

Remove Require Import Compiler in ErrorsC.v. It corrupts namespaces too much.

alxest commented 4 years ago

When I type Search AST.prog_defmap. in Fib01proof, I should'nt see any Unreadglobproof... things.

alxest commented 4 years ago

When I type Locate state after Require Import RUSC AdequacyLocal, it shouldn't show the languages.