bug fix in Track definition

[helm.git] / matita / contribs / LOGIC / datatypes / Proof.ma

diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma
index 357b044f5a448494fed4a9de7a50d612993d9ac0..f6260b0264c1e770df5c07a76a18ffe4f4bae4b9 100644 (file)
--- a/matita/contribs/LOGIC/datatypes/Proof.ma
+++ b/matita/contribs/LOGIC/datatypes/Proof.ma
@@ -23,7 +23,7 @@ include "preamble.ma".
 
 inductive Proof: Type \def
    | lref: Nat \to Proof                       (* projection         *)
-   | parx: Nat \to Proof                       (*                    *)
+   | prin: Nat \to Proof                       (* pos rel inhabitant *)
    | impw: Proof \to Proof                     (* weakening          *)
    | impr: Proof \to Proof                     (* right introduction *)
    | impi: Proof \to Proof \to Proof \to Proof (* left introduction  *)