aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--PROBLEMES8
1 files changed, 8 insertions, 0 deletions
diff --git a/PROBLEMES b/PROBLEMES
index 43be1f5f40..16a6a829f2 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -1,3 +1,11 @@
+Variable + Record => clash. Exemple:
+======================================================================
+Section S.
+Variable F:Set.
+Record R [ F:Set; x:F ] : Set := { c : x=x }.
+ => Error: new_isevar_sign: two vars have the same name
+======================================================================
+
Hints Resolve fait une anomalie si la constante n'existe pas
--> CORRIGÉ