]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationUtil.ml
* various bug fix related to the environment returned when a match
[helm.git] / helm / ocaml / cic_notation / cicNotationUtil.ml
index 630fb436168109ea56c3dff6302f74a80d78b64f..740a9c1464af06c1a335c55a03ed09c7df9555cc 100644 (file)
@@ -166,10 +166,11 @@ let visit_layout k = function
 
 let visit_magic k = function
   | List0 (t, l) -> List0 (k t, l)
-  | List1 (t, l) -> List1 (k t, l )
+  | List1 (t, l) -> List1 (k t, l)
   | Opt t -> Opt (k t)
   | Fold (kind, t1, names, t2) -> Fold (kind, k t1, names, k t2)
   | Default (t1, t2) -> Default (k t1, k t2)
+  | If (t1, t2) -> If (k t1, k t2)
 
 let variables_of_term t =
   let rec vars = ref [] in