X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcontribs%2FLOGIC%2Fdatatypes%2FProof.ma;fp=matita%2Fcontribs%2FLOGIC%2Fdatatypes%2FProof.ma;h=f6260b0264c1e770df5c07a76a18ffe4f4bae4b9;hb=4d3fcebb0b24901b69f54d0eaf067885a80dcae0;hp=357b044f5a448494fed4a9de7a50d612993d9ac0;hpb=2a85b279378df4193bbe927e3cdbaffd7d229279;p=helm.git

diff --git a/matita/contribs/LOGIC/datatypes/Proof.ma b/matita/contribs/LOGIC/datatypes/Proof.ma
index 357b044f5..f6260b026 100644
--- 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  *)