cicInspect: node count fixed

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Legacy-2 / preamble.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
index b9b749816f0a47d6b69ab5d130a1e940d0d32858..0666938e899ecbd2702454f0995f6e0ecb8984f3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Legacy-1/definitions.ma".
+include "Legacy-1/theory.ma".
 
 default "equality"
  cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind
@@ -42,7 +42,7 @@ interpretation "Coq 7.3.1 logical not" 'not x = (cic:/matita/LAMBDA-TYPES/Legacy
 interpretation "Coq 7.3.1 exists" 'exists \eta.x = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/ex.ind#xpointer(1/1) _ x).
 interpretation "Coq 7.3.1 natural 'less or equal to'" 'leq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/le.ind#xpointer(1/1) x y).
 interpretation "Coq 7.3.1 natural 'less than'" 'lt x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/lt.con x y).
-interpretation "Coq 7.3.1 leibnitz's equality" 'eq x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) _ x y).
+interpretation "Coq 7.3.1 leibnitz's equality" 'eq t x y = (cic:/matita/LAMBDA-TYPES/Legacy-1/coq/defs/eq.ind#xpointer(1/1) t x y).
 
 alias symbol "plus" = "Coq 7.3.1 natural plus".
 alias symbol "minus" = "Coq 7.3.1 natural minus".