I have my own functions collection called all_value. When i call it, then am facing following problem
Require Export all_value.
I am using function "current" it appears as all_value.current a b=true . Want to look like
current a b=true .
Already i have "Require Export all_value". Now i have added "Require Import all_valu". But still every thing is same. No improvement.
What Coq says when you enter :
Locate current. Import all_value. Locate current.
Last updated: Oct 04 2023 at 23:01 UTC