From 105db906ae45e792d1caeeb2e3fb7f69944b2caa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 12:53:41 +0200
Subject: - Fixes for canonical structure resolution (check that the initial
 term indeed unifies with the projected term, keeping track of universes). -
 Fix the [unify] tactic to fail properly. - Fix unification to disallow
 lowering a global Type(i) universe to Prop or Set.

---
 test-suite/success/Funind.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite')

diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index ccce3bbe10..1ed2221ccd 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -23,6 +23,7 @@ Function ftest (n m : nat) : nat :=
          end
   | S p => 0
   end.
+(* MS: FIXME: apparently can't define R_ftest_complete *)
 
 Lemma test1 : forall n m : nat, ftest n m <= 2.
 intros n m.
-- 
cgit v1.2.3