metacoq icon indicating copy to clipboard operation
metacoq copied to clipboard
verified publisher icon MetaCoq

Enable tmDefinition to generate local definitions

Open gmalecha opened this issue 6 years ago • 0 comments

Per discussion on the gitter.

Coq trunk contains:

(* coq trunk *)
type import_status = ImportDefaultBehavior | ImportNeedQualified
type locality = Discharge | Global of import_status
(* coq < 8.9 *)
type locality = Global | Local

We will expose the new interface and provide definitions that translate Discharge into Global.

gmalecha avatar Sep 26 '19 14:09 gmalecha