Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Looking up definitions from inside an ml plugin

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Looking up definitions from inside an ml plugin


Chronological Thread 
  • From: Kenneth Roe <kendroe AT hotmail.com>
  • To: Coq-Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Looking up definitions from inside an ml plugin
  • Date: Thu, 16 Nov 2017 15:34:11 +0000
  • Accept-language: en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=kendroe AT hotmail.com; spf=Pass smtp.mailfrom=kendroe AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM03-CO1-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:T8zsYxHdEvU2MhvUxTEplp1GYnF86YWxBRYc798ds5kLTJ76ocmwAkXT6L1XgUPTWs2DsrQf1LqQ7viocFdDyKjCmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TXhpQIVTz74LE9eIvn/UtrZiN3y3OSv8bXSZR9JjXyze+UhAg+xqFDyu88QjJdiYpw2x1OdoXZOd/5RyEtoIk6Wlhf4oMy3+cgwoGxrp/s9+psYAu3BdKMiQOkAAQ==
  • Spamdiagnosticmetadata: NSPM
  • Spamdiagnosticoutput: 1:99

I am developing an ml tactic, "arewrite".  Inside a Coq source file where I use the tactic, I have the following code:

Require Import AdvancedRewrite.advancedRewrite.


Inductive x := | Const : nat -> x | XX : x -> x -> x.


Theorem test7: forall x, x=Const 4.

Proof.

    intros.

    arewrite.

Abort.


From inside the "arewrite" ml source code, I have the following code to try and lookup the definition of "x":

    let i = ... s ... (* s contains the string "C_Top.x" *)

    let d = Environ.lookup_mind i env


Can someone fill in what I need for the first line to properly form the identifier "i"?

                                         - Ken



Archive powered by MHonArc 2.6.18.

Top of Page