- 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.

1 files changed, 1 insertions, 0 deletions

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.