...

[helm.git] / helm / software / components / acic_content / cicNotationUtil.ml

diff --git a/helm/software/components/acic_content/cicNotationUtil.ml b/helm/software/components/acic_content/cicNotationUtil.ml
index f331b79ca8d2da4c3a545c54b6789dcb1eb59a7b..5c3936d93b0771d5feb8f52c9dd16327a629c22d 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -35,8 +35,8 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Ast.Case (term, indtype, typ, patterns) ->
         Ast.Case (k term, indtype, aux_opt typ, aux_patterns patterns)
     | Ast.Cast (t1, t2) -> Ast.Cast (k t1, k t2)
-    | Ast.LetIn (var, t1, t2) ->
-        Ast.LetIn (aux_capture_variable var, k t1, k t2)
+    | Ast.LetIn (var, t1, t3) ->
+        Ast.LetIn (aux_capture_variable var, k t1, k t3)
     | Ast.LetRec (kind, definitions, term) ->
         let definitions =
           List.map
@@ -67,8 +67,11 @@ let visit_ast ?(special_k = fun _ -> assert false) k =
     | Some term -> Some (k term)
   and aux_capture_variable (term, typ_opt) = k term, aux_opt typ_opt
   and aux_patterns patterns = List.map aux_pattern patterns
-  and aux_pattern ((head, hrefs, vars), term) =
-    ((head, hrefs, List.map aux_capture_variable vars), k term)
+  and aux_pattern =
+   function
+      Ast.Pattern (head, hrefs, vars), term ->
+        Ast.Pattern (head, hrefs, List.map aux_capture_variable vars), k term
+    | Ast.Wildcard, term -> Ast.Wildcard, k term
   and aux_subst (name, term) = (name, k term)
   and aux_substs substs = List.map aux_subst substs
   in
@@ -82,11 +85,13 @@ let visit_layout k = function
   | Ast.Over (t1, t2) -> Ast.Over (k t1, k t2)
   | Ast.Atop (t1, t2) -> Ast.Atop (k t1, k t2)
   | Ast.Frac (t1, t2) -> Ast.Frac (k t1, k t2)
+  | Ast.InfRule (t1, t2, t3) -> Ast.InfRule (k t1, k t2, k t3)
   | Ast.Sqrt t -> Ast.Sqrt (k t)
   | Ast.Root (arg, index) -> Ast.Root (k arg, k index)
   | Ast.Break -> Ast.Break
   | Ast.Box (kind, terms) -> Ast.Box (kind, List.map k terms)
   | Ast.Group terms -> Ast.Group (List.map k terms)
+  | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)
@@ -133,7 +138,7 @@ let names_of_term t =
   let aux = function
     | Ast.NumVar s
     | Ast.IdentVar s
-    | Ast.TermVar s -> s
+    | Ast.TermVar (s,_) -> s
     | _ -> assert false
   in
     List.map aux (variables_of_term t)
@@ -184,9 +189,9 @@ let meta_names_of_term term =
         aux term ;
         aux_opt outty_opt ;
         List.iter aux_branch patterns
-    | Ast.LetIn (_, t1, t2) ->
+    | Ast.LetIn (_, t1, t3) ->
         aux t1 ;
-        aux t2
+        aux t3
     | Ast.LetRec (_, definitions, body) ->
         List.iter aux_definition definitions ;
         aux body
@@ -213,8 +218,10 @@ let meta_names_of_term term =
   and aux_branch (pattern, term) =
     aux_pattern pattern ;
     aux term
-  and aux_pattern (head, _, vars) = 
-    List.iter aux_capture_var vars
+  and aux_pattern =
+   function
+      Ast.Pattern (head, _, vars) -> List.iter aux_capture_var vars
+    | Ast.Wildcard -> ()
   and aux_definition (params, var, term, decrno) =
     List.iter aux_capture_var params ;
     aux_capture_var var ;
@@ -224,7 +231,7 @@ let meta_names_of_term term =
   and aux_variable = function
     | Ast.NumVar name -> add_name name
     | Ast.IdentVar name -> add_name name
-    | Ast.TermVar name -> add_name name
+    | Ast.TermVar (name,_) -> add_name name
     | Ast.FreshVar _ -> ()
     | Ast.Ascription _ -> assert false
   and aux_magic = function