]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/contribs/lambdadelta/bin/recomm/recommGcdGroundRelocation.ml
update in ground
[helm.git] / matita / matita / contribs / lambdadelta / bin / recomm / recommGcdGroundRelocation.ml
index 349cf6b36f9df5dadf6329557d2f73047c0e1303..a146ffc983aa81569c4c014574bfcaf1232ae536 100644 (file)
@@ -4,7 +4,7 @@ module R = RecommPccFor
 let step k st outs ins =
   if st <> T.OO then k st outs ins else
   match ins with
-  | "GENERIC" :: "RELOCATION" :: "MAPS" :: tl -> k T.OK ("MAPS" :: "RELOCATION" :: "GENERIC" :: outs) tl
+  | "PARTIAL" :: "RELOCATION" :: "MAPS" :: tl -> k T.OK ("MAPS" :: "RELOCATION" :: "PARTIAL" :: outs) tl
   | "FINITE" :: "RELOCATION" :: "MAPS" :: "WITH" :: "PAIRS" :: tl -> k T.OK ("PAIRS" :: "WITH" :: "MAPS" :: "RELOCATION" :: "FINITE" :: outs) tl
   | "FINITE" :: "RELOCATION" :: "MAPS" :: tl -> k T.OK ("MAPS" :: "RELOCATION" :: "FINITE" :: outs) tl
   | _ -> k T.OO outs ins