]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationParser.ml
snapshot (added typed environment in 2 -> 1 conversion)
[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml
index 767aa3d1579d80ae74ff5ddda550f00251fe75c8..fa8b65ed0a4f3b24f34f74c4f80928e2d0db6cfd 100644 (file)
@@ -85,34 +85,34 @@ let make_action action bindings =
     | NoBinding :: tl ->
         prerr_endline "aux: none";
         Gramext.action (fun _ -> aux vl tl)
-    (* LUCA: DEFCON 2 BEGIN *)
+    (* LUCA: DEFCON 5 BEGIN *)
     | Binding (name, TermType) :: tl ->
         prerr_endline "aux: term";
         Gramext.action
-          (fun (v:term) -> aux ((name, (TermType, (TermValue v)))::vl) tl)
+          (fun (v:term) -> aux ((name, (TermType, TermValue v))::vl) tl)
     | Binding (name, StringType) :: tl ->
         prerr_endline "aux: string";
         Gramext.action
           (fun (v:string) ->
-            aux ((name, (StringType, (StringValue v))) :: vl) tl)
+            aux ((name, (StringType, StringValue v)) :: vl) tl)
     | Binding (name, NumType) :: tl ->
         prerr_endline "aux: num";
         Gramext.action
-          (fun (v:string) -> aux ((name, (NumType, (NumValue v))) :: vl) tl)
+          (fun (v:string) -> aux ((name, (NumType, NumValue v)) :: vl) tl)
     | Binding (name, OptType t) :: tl ->
         prerr_endline "aux: opt";
         Gramext.action
           (fun (v:'a option) ->
-            aux ((name, (OptType t, (OptValue v))) :: vl) tl)
+            aux ((name, (OptType t, OptValue v)) :: vl) tl)
     | Binding (name, ListType t) :: tl ->
         prerr_endline "aux: list";
         Gramext.action
           (fun (v:'a list) ->
-            aux ((name, (ListType t, (ListValue v))) :: vl) tl)
+            aux ((name, (ListType t, ListValue v)) :: vl) tl)
     | Env _ :: tl ->
         prerr_endline "aux: env";
         Gramext.action (fun (v:CicNotationEnv.t) -> aux (v @ vl) tl)
-    (* LUCA: DEFCON 2 END *)
+    (* LUCA: DEFCON 5 END *)
   in
     aux [] (List.rev bindings)