fixed -debug

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / ac_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index d23ed4e1a4272d26fb6dc8b62e67f4c593ad9f35..6a5b86cf15f1e29f4677dfb994295f16a62b0003 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -41,5 +41,5 @@ record AC: Type \def {
 coercion ac. 
 
 inductive eq (A:AC) (a:A): A \to Prop \def
-   | eq_refl:   acin ? a \to eq A a a.
+   | eq_refl:   acin ? a \to eq ? a a.
 (*   | eq_sing_r: \forall b,c. eq A a b \to aceq A b c \to eq A a c. *)