coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

[Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/16/2017
- Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
  - Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/16/2017
    - Message not available
      - Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/17/2017
        
        Re: [Coq-Club] Looking up definitions from inside an ml plugin, Talia Ringer, 11/17/2017
        
        Re: [Coq-Club] Looking up definitions from inside an ml plugin, Kenneth Roe, 11/19/2017
        
        Re: [Coq-Club] Looking up definitions from inside an ml plugin, Matthieu Sozeau, 11/19/2017