File: bug_2837.v

package info (click to toggle)
coq-doc 8.20.0-2
  • links: PTS, VCS
  • area: non-free
  • in suites: forky, sid, trixie
  • size: 46,708 kB
  • sloc: ml: 234,429; sh: 4,686; python: 3,359; ansic: 2,644; makefile: 842; lisp: 172; javascript: 87; xml: 24; sed: 2
file content (16 lines) | stat: -rw-r--r-- 411 bytes parent folder | download | duplicates (5) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
 
Require Import JMeq.

Axiom test : forall n m : nat, JMeq n m.

Goal forall n m : nat, JMeq n m.

(* I) with no intros nor variable hints, this should produce a regular error
      instead of Uncaught exception Failure("nth"). *)
Fail rewrite test.

(* II) with intros but indication of variables, still an error *)
Fail (intros; rewrite test).

(* III) a working variant: *)
intros; rewrite (test n m).
Abort.