X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fpaths%2Fpath.ma;h=7105c519ff3dede78304ac4e2a978a49d69559e9;hb=81fc94f4f091ec35d41e2711207218d255b75273;hp=c9f4cc244e06b3818656bb748cc8478b54746976;hpb=39aab7babf51252cecb81a66af82fe797e8dcbe7;p=helm.git

diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma
index c9f4cc244..7105c519f 100644
--- a/matita/matita/contribs/lambda/paths/path.ma
+++ b/matita/matita/contribs/lambda/paths/path.ma
@@ -16,7 +16,7 @@ include "terms/term.ma".
 
 (* PATH *********************************************************************)
 
-(* Policy: path step metavariables: c *)
+(* Policy: path step metavariables: o *)
 (* Note: this is a step of a path in the tree representation of a term:
          rc (rectus)  : proceed on the argument of an abstraction
          sn (sinister): proceed on the left argument of an application
@@ -28,7 +28,7 @@ inductive step: Type[0] ≝
 | dx: step
 .
 
-definition is_dx: predicate step ≝ λc. dx = c.
+definition is_dx: predicate step ≝ λo. dx = o.
 
 (* Policy: path metavariables: p, q *)
 (* Note: this is a path in the tree representation of a term, heading to a redex *)