All weakly positive types but imbricated ones are now accepted

[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 1ddd5c9c3b1572c74034fb70b4f2563867ee6786..60fe6357d5f1c4c878187f12e086c6ce49cd3006 100644 (file)
--- a/helm/software/components/acic_content/cicNotationUtil.ml
+++ b/helm/software/components/acic_content/cicNotationUtil.ml
@@ -99,6 +99,7 @@ let visit_layout k = function
   | Ast.Group terms -> Ast.Group (List.map k terms)
   | Ast.Mstyle (l, term) -> Ast.Mstyle (l, List.map k term)
   | Ast.Mpadded (l, term) -> Ast.Mpadded (l, List.map k term)
+  | Ast.Maction terms -> Ast.Maction (List.map k terms)
 
 let visit_magic k = function
   | Ast.List0 (t, l) -> Ast.List0 (k t, l)
@@ -361,7 +362,8 @@ let fresh_id () =
   !fresh_index
 
   (* TODO ensure that names generated by fresh_var do not clash with user's *)
-let fresh_name () = "η" ^ string_of_int (fresh_id ())
+  (* FG: "η" is not an identifier (it is rendered, but not be parsed) *)
+let fresh_name () = "eta" ^ string_of_int (fresh_id ())
 
 let rec freshen_term ?(index = ref 0) term =
   let freshen_term = freshen_term ~index in