coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] difference between env and context

From: shengyu shen <shengyushen AT icloud.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] difference between env and context
Date: Wed, 09 Dec 2015 03:28:47 +0000 (GMT)
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=shengyushen AT icloud.com; spf=Pass smtp.mailfrom=shengyushen AT icloud.com; spf=None smtp.helo=postmaster AT pv33p04im-asmtp002.me.com
Ironport-phdr: 9a23:rHlyWRL0+92WAvfZcNmcpTZWNBhigK39O0sv0rFitYgUKf7xwZ3uMQTl6Ol3ixeRBMOAu6wC07KempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRMiK14ye7KObxd76W01wnj2zYLd/fl2djD76kY0ou7ZkMbs70RDTo3FFKKx8zGJsIk+PzV6nvp/jtM0rzyMFsPU4ssVETK/SfqIiTLUeAi51HXoy4ZjwtRTFQhqSrmAcX2NexgFIDg7K/QzhXpr3mirxsu1g1G+ROsigHuN8Yiir86o+EEygsywALTNsqGw=

Dear all:

what is the difference between context and env in coq?

It seems that env include all the system theory loaded by Require Import , while context seems to be the set of all user declaration and intermediate lemmas.

Shen

[Coq-Club] difference between env and context, shengyu shen, 12/09/2015