- some additions and renaming ...

[helm.git] / matita / matita / contribs / lambda / paths / path.ma

diff --git a/matita/matita/contribs/lambda/paths/path.ma b/matita/matita/contribs/lambda/paths/path.ma
index c9f4cc244e06b3818656bb748cc8478b54746976..7105c519ff3dede78304ac4e2a978a49d69559e9 100644 (file)
--- 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 *)