]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/src/text/txtTxt.ml
when sort inclusion is enabled, we can produce conversion constraints in xml
[helm.git] / helm / software / lambda-delta / src / text / txtTxt.ml
index d2c85cb921a9ac4d3e492b0e1b70dd03d0367fbc..fe0988401a3a803c74ee9696c3b418fc7db5163c 100644 (file)
@@ -23,7 +23,7 @@ let rec contract f = function
       contract f tt      
    | T.Impl (n, true, id, w, t)  -> 
       let f = function
-         | T.Bind (n, T.Abst [xw], T.Bind (_, T.Abst xws, tt)) ->
+         | T.Bind (_, T.Abst [xw], T.Bind (n, T.Abst xws, tt)) ->
             f (T.Bind (n, T.Abst (xw :: xws), tt))
         | tt                                            -> f tt
       in