added a (for the moment) dummy field _subst to ProofengineTypes.proof.

[helm.git] / helm / software / matita / dama / ordered_sets.ma

diff --git a/helm/software/matita/dama/ordered_sets.ma b/helm/software/matita/dama/ordered_sets.ma
index 27b10aeefbac510bfc7d65a7d4ae70873a6483a0..1ca191339b697514c39b171ed9111ef8c6a1003c 100644 (file)
--- a/helm/software/matita/dama/ordered_sets.ma
+++ b/helm/software/matita/dama/ordered_sets.ma
@@ -692,4 +692,4 @@ qed.
 definition lt ≝ λO:ordered_set.λa,b:O.a ≤ b ∧ a ≠ b.
 
 interpretation "Ordered set lt" 'lt a b =
- (cic:/matita/ordered_sets/lt.con _ _ a b).
+ (cic:/matita/ordered_sets/lt.con _ a b).