Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Environ.NotEvaluableConst exception #35

Closed
sayon opened this issue Mar 17, 2016 · 2 comments
Closed

Environ.NotEvaluableConst exception #35

sayon opened this issue Mar 17, 2016 · 2 comments
Assignees
@gares
Labels
kind: bug Issue which describe bugs

Comments

@sayon
Copy link

sayon commented Mar 17, 2016 

From mathcomp Require Import ssreflect.all_ssreflect.
Definition cst2 {A B : Type} (a: A ) (H: A= B ) : B.
  rewrite <-H.
  exact a.
Qed. (* I know it should be 'defined' instead*)

Lemma test: cst2 4 Logic.eq_refl = 4.
  rewrite /cst2.

results in

Anomaly: Uncaught exception Environ.NotEvaluableConst(1). Please report.
@gares gares self-assigned this Mar 17, 2016
@gares gares added the kind: bug Issue which describe bugs label Mar 17, 2016
@gares
Copy link
Member

gares commented Mar 17, 2016

Thanks for reporting. I'll make it spit out a nicer error message.

Best,

@gares gares added this to the 1.7 milestone Jan 19, 2017
@gares gares removed this from the 1.7 milestone Apr 17, 2018
@proux01
Copy link
Contributor

proux01 commented Apr 20, 2022

It now (Coq 8.15) reports:

Error: cst2 is opaque.

which sounds nice.

Should we close?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@gares gares

Labels
kind: bug Issue which describe bugs
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@CohenCyril @gares @sayon @proux01