coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Turning an evar into a goal?

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Turning an evar into a goal?
Date: Sat, 01 Apr 2017 18:20:54 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt0-f172.google.com
Ironport-phdr: 9a23:APF7rxKe/RNlgTtPDNmcpTZWNBhigK39O0sv0rFitYgRKvTxwZ3uMQTl6Ol3ixeRBMOAuq4C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwpFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygHOTA382/Zl9J+g75ArR27uxBy2ZTZbJ2JOPd8eK7WYNMURXBGXsZUTyFPBpmzb5AID+oHIO1WrpP9p1wVrRulGAKhA+HvxSVThn/x26063P4hEQbd3Aw7G98Dq3vUrNDvO6cTVeC51rXHzTLGb/5P3zr29YvGcgg5rP2SQb59ddDdxEovGg/fkFmctI3oMymI2ukPrWSW6fdrW/i1hG49sQ5xpyCixscyhYnNgYIY0lXE+j94wIYxPNG4UVJ7bcK9HJteqi2XNZV6TtktQ2FvvyY6xbkGtoChcCcWz5QnwgbTa/2Bc4eW/hLuTPidLSt8iX5/e7+yhwy+/Va9xuD9TMW4zVRHojRdntnJrH8N1hjT6sadSvt6+0eswTSP2BrI6uFDJ0A0mrDbK5k6wr4rkpceqkvDHirsl0X3iK+abFkr+u+t6+j/eLXpuoecN5NoigH5Kqkhhsu/Af0hPgcSW2ib5P+z2ab4/Uz5RbVKluc5nrPYsJDcP8Qbp7S2DxVb0oY5uF6DCGKt181dln0aJhoRcxWeyoPtJlvmIfbiDP75jU76wxlxwPWTHLT6BZOFAWLEi6ypKbR08ElaxxA01ssOz51RA7AFZvn0Xxmi55TjEhYlPlnskK7cA9Jn29ZGVA==

Say I have an Ltac variable x such that [is_evar x] succeeds. How do I get a goal corresponding to x, in an Ltac script (without vernaculars)? I tried making a new goal and unifying the evar of that goal with x, but that fails with a "not well typed in the context of x" message, because I have different hypotheses.

Thanks,

Jason

[Coq-Club] Turning an evar into a goal?, Jason Gross, 04/01/2017
- Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/01/2017
  - Re: [Coq-Club] Turning an evar into a goal?, Jason Gross, 04/03/2017
    - Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/03/2017
      - Re: [Coq-Club] Turning an evar into a goal?, Jason Gross, 04/03/2017
        
        Re: [Coq-Club] Turning an evar into a goal?, Jonathan Leivent, 04/03/2017