List archive

• RE: [ssreflect] Question about ssreflect, Georges Gonthier, 06/03/2014
• [ssreflect] ? pattern does not work with case, Jason Gross, 06/04/2014
  • Re: [ssreflect] ? pattern does not work with case, Enrico Tassi, 06/04/2014
• [ssreflect] Time-annotated sources for the non-trunk versions of ssr, Jason Gross, 06/04/2014
• [ssreflect] Ssreflect sometimes breaks the [a : b] notation of Coq, Jason Gross, 06/06/2014
  • Message not available
    • Message not available
      • RE: [ssreflect] Ssreflect sometimes breaks the [a : b] notation of Coq, Georges Gonthier, 06/06/2014
• [ssreflect] Dependent variant of case/boolP?, Jason Gross, 06/11/2014
  • Re: [ssreflect] Dependent variant of case/boolP?, Assia Mahboubi, 06/11/2014
    • Re: [ssreflect] Dependent variant of case/boolP?, Jason Gross, 06/11/2014
  • Re: [ssreflect] Dependent variant of case/boolP?, Enrico Tassi, 06/11/2014
    • Re: [ssreflect] Dependent variant of case/boolP?, Jason Gross, 06/11/2014
      • Re: [ssreflect] Dependent variant of case/boolP?, Enrico Tassi, 06/11/2014
• [ssreflect] Anomaly: Uncaught exception Environ.NotEvaluableConst(1). Please report., Jason Gross, 06/11/2014
  • Re: [ssreflect] Anomaly: Uncaught exception Environ.NotEvaluableConst(1). Please report., Maxime Dénès, 06/11/2014
    • Re: [ssreflect] Anomaly: Uncaught exception Environ.NotEvaluableConst(1). Please report., Enrico Tassi, 06/11/2014
• [ssreflect] bigop question, Laurence Rideau, 06/11/2014
  • RE: [ssreflect] bigop question, Georges Gonthier, 06/11/2014
• [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed. Please report., Jason Gross, 06/12/2014
  • Re: [ssreflect] Anomaly: File "tactics/tacinterp.ml", line 1801, characters 35-41: Assertion failed. Please report., Enrico Tassi, 06/12/2014
• [ssreflect] Ssreflect (1.4) breaks Ltac's type of notation, Jason Gross, 06/18/2014
  • RE: [ssreflect] Ssreflect (1.4) breaks Ltac's type of notation, Georges Gonthier, 06/19/2014
    • Re: [ssreflect] Ssreflect (1.4) breaks Ltac's type of notation, Jason Gross, 06/19/2014
• [ssreflect] a new question about bigop (for Sophie...), Laurence Rideau, 06/18/2014
  • RE: [ssreflect] a new question about bigop (for Sophie...), Georges Gonthier, 06/19/2014
• [ssreflect] Differences between ssr's rewrite and Coq's rewrite?, Jason Gross, 06/19/2014
  • Re: [ssreflect] Differences between ssr's rewrite and Coq's rewrite?, Enrico Tassi, 06/19/2014
    • Re: [ssreflect] Differences between ssr's rewrite and Coq's rewrite?, Assia Mahboubi, 06/19/2014
• [ssreflect] Why does [case/(@id (and _ _))] tell me that [and] is not an inductive product?, Jason Gross, 06/26/2014
  • Re: [ssreflect] Why does [case/(@id (and _ _))] tell me that [and] is not an inductive product?, Enrico Tassi, 06/26/2014
    • Re: [ssreflect] Why does [case/(@id (and _ _))] tell me that [and] is not an inductive product?, Jason Gross, 06/26/2014

Archive powered by MHonArc 2.6.18.