added records

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 9510287450ce9398b46e6069387480e6f30b7282..a7d43bb45f75461cda893201a49459bc458f0dda 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -472,7 +472,22 @@ EXTEND
       let ind_types = fst_ind_type :: tl_ind_types in
       (params, ind_types)
   ] ];
-
+  
+  record_spec: [ [
+    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+     SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; PAREN "{" ; 
+     fields = LIST0 [ 
+       name = IDENT ; SYMBOL ":" ; ty = term -> (name,ty) 
+     ] SEP SYMBOL ";"; PAREN "}" -> 
+      let params =
+        List.fold_right
+          (fun (names, typ) acc ->
+            (List.map (fun name -> (name, typ)) names) @ acc)
+          params []
+      in
+      (params,name,typ,fields)
+  ] ];
+  
   macro: [
     [ [ IDENT "quit"  ] -> TacticAst.Quit loc
 (*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
@@ -572,6 +587,8 @@ EXTEND
         TacticAst.Coercion (loc, CicAst.Uri (name,Some []))
     | [ IDENT "alias"   ]; spec = alias_spec ->
         TacticAst.Alias (loc, spec)
+    | [ IDENT "record" ]; (params,name,ty,fields) = record_spec ->
+        TacticAst.Record (loc, params,name,ty,fields)
   ]];
 
   executable: [