diff --git a/lib/formula.ml b/lib/formula.ml
index 8f86b8481dbf2fdfec8796a7cd47378fdec64e98..91122f2a7276341880429aa4a0b3f3ebbdb7298b 100644
--- a/lib/formula.ml
+++ b/lib/formula.ml
@@ -23,6 +23,7 @@ type t =
   | Record of t list
   | RecordDef of t list
   | Tuple of t list
+  | Set of t list (*modif*)
   | Raw of string
 [@@deriving show,eq,ord,yojson { strict = true }]
 
@@ -50,6 +51,7 @@ let priority f =
   | Record _ -> 0
   | RecordDef _ -> 0
   | Tuple(_) -> 0
+  | Set(_) -> 0
   | Raw _ -> 0
   | Let (_,_,_) -> 0
   | Infix (_,_,_) -> 108 (* so that "a < 4 /\ A >= 9" works *)
@@ -132,6 +134,7 @@ let rec pretty fmt form =
   | Record (lst) -> Format.fprintf fmt "@[<v 2>{| %a |}@]" (Pp.print_list Pp.semi fp) lst
   | RecordDef (lst) -> Format.fprintf fmt "@[<v 2>{ %a }@]" (Pp.print_list Pp.semi fp) lst
   | Tuple (lst) -> Format.fprintf fmt "@[{ %a }@]" (Pp.print_list Pp.comma fp) lst
+  | Set (lst) -> Format.fprintf fmt "@[( %a )@]" (Pp.print_list Pp.comma fp) lst
   | Let(id, f1, f2) -> Format.fprintf fmt "@[<v>let %s := %a@ in @[<v>%a@]@]"
                        id 
                        fp f1 
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 23fcbb749fc5055a41cc4ea7fb867ba77c667659..faebedd0a5743e299376fa53de2793fba61d14eb 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -105,7 +105,7 @@ let rec expr_to_coq (r : expr) : Formula.t =
       | Cons (e1,e2) -> App(Raw("cons"), ([expr_to_coq e1;expr_to_coq e2]))
       | Fun (s,e) -> Fun(Some s, expr_to_coq e)
       | App (f,arg) -> App(expr_to_coq f, [expr_to_coq arg])
-      | Set s -> Raw("(" ^ String.concat "," (set_to_coq s) ^")")
+      | Set s -> Set (set_to_coq s)
       | Point (m,f) -> let c = List.assoc_opt m Module.correspondance in 
                        (match c with
                         |None -> raise(Failure("Problem: "^m^" unknow"))
@@ -114,10 +114,10 @@ let rec expr_to_coq (r : expr) : Formula.t =
                                   |  Some x' -> x')
                         )
       | _ ->  Raw("Not Implemented")
-      and  set_to_coq (s:expr set) : string list =
+      and  set_to_coq (s:expr set) : Formula.t list =
         match s with 
         | Vide -> []
-        | Some (s',e) -> string_of_expression e :: set_to_coq s'
+        | Some (s',e) ->expr_to_coq e :: set_to_coq s'
       
 
 (**[instance_R_R2 s d] generates the coq code to instance R and R2
@@ -171,7 +171,7 @@ let instance_space (s: space) (d : information list): stmt list =
 let instance_updfunc_rigid (valret : string) (d: information list):stmt list =
   if not(get_space d = "Ring") then
     Instance("UpdFun",Raw("update_function ("^valret^") (Similarity.similarity location) unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
-    ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
+    ::(*RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::*)[]
   else 
     Instance("FC",App(Cst "frame_choice",[Raw("(Z * bool)")]),Raw(" {frame_choice_bijection :=
         fun nb => if snd nb then Ring.sym (fst nb) else Ring.trans (fst nb);
diff --git a/lib/parser.mly b/lib/parser.mly
index fc3655f8035bcbaeb9df3f9c5f90a9d4f55a6e59..294cdc485c907643a2f83acceefe32d254547418 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -266,6 +266,8 @@ id :
 set :
     | e = expression COMMA s = set {Some(s,e)} 
     | e = expression {Some(Vide,e)} 
+     | e = KEYWORD COMMA s = set {Some(s,Var e)} 
+    | e = KEYWORD {Some(Vide,Var e)} 
     | {Vide}
 
 %inline binop :