Ssreflect Users Discussion List

[Jose Grimm <>]

The following input;

Require Import ssreflect ssrbool eqtype ssrnat.

Goal (forall n m:nat, n = m -> n = n).
move => n m H.
rewrite [X in X = _] H.

gives;

1 subgoals, subgoal 1 (ID 14)

  n : nat
  m : nat
  H : n = m
  ============================
   m = m

(dependent evars:)


where I expected the goal to be m = n.

I'm using coq8.4, together with the ssreflect from coqfinitgroup/trunk

The Coq Proof Assistant, version 8.4 (September 2012)
compiled on Sep 18 2012 18:24:06 with OCaml 3.12.0


URL: https://scm.gforge.inria.fr/svn/coqfinitgroup/trunk
Last Changed Rev: 4165
Last Changed Date: 2012-12-12 10:12:42 +0100 (Wed, 12 Dec 2012)


Jose'

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature