diff --git a/lib/ast.ml b/lib/ast.ml
index 5ddc16b0a68070ed68e920905455f0ba960dbf3a..0b3e3f45391869aba38f87ef142f23ec1ee489df 100644
--- a/lib/ast.ml
+++ b/lib/ast.ml
@@ -202,9 +202,16 @@ type information =
   | Roles of (int * string) list
   | Share of share
 
+(*TODO: a modif selon l'implementation de graph utilisé*)
+type graph = Graph of string
+
+type measure = Measure of int * graph
+
+
+
 (* Une description c'est 1: description de l'environnement et des capacites des robot
 	 											 2: robogram *)
-type description = Description of ((information list) * (expr list))
+type description = Description of ((information list) * (expr list) * measure)
 
 
 (*FONCTION SUR LES SETS*)
@@ -354,7 +361,7 @@ let string_of_rigidity (r: rigidity) : string =
 
 let rec string_of_description (desc:description) : string =
   match desc with
-  | Description (infos,robogram) -> 
+  | Description (infos,robogram,_) -> 
         "Description environnement:\n" ^String.concat "\n" (List.map string_of_information infos)
         ^"\nRobogram : \n " ^  String.concat "\n" (List.map string_of_expression robogram)
 and string_of_information (info: information) : string =
@@ -404,7 +411,7 @@ let check_description (d : description) :bool =
 			let unique f d = List.length (List.filter f d) = 1
 			in 
 			match d with 
-			| Description (d',_) -> if not(unique info_sync d')
+			| Description (d',_,_) -> if not(unique info_sync d')
                                   then (print_endline "Error: Problem of defining sync"; false)
 													    else (
                                   if not(unique info_space d') 
@@ -418,14 +425,14 @@ let check_description (d : description) :bool =
     *)
 let get_sensors (d : description) : sensor list =
   match d with 
-  | Description(d', _) -> (match List.find_opt (fun x -> match x with Sensors _ -> true | _-> false) d' with 
+  | Description(d', _,_) -> (match List.find_opt (fun x -> match x with Sensors _ -> true | _-> false) d' with 
                           Some (Sensors s) -> s 
                           | _ -> raise(Failure("Error: Not find Sensors")))
 
 (**[get_robot d] Renvoie la liste des champs robot contenu dans la descritpion [d]
     @param description
     @return [field list]*)
-let get_robot (Description(d', _) : description) : field list =
+let get_robot (Description(d', _,_) : description) : field list =
   match List.find_opt (fun x -> match x with Robot _ -> true | _-> false) d' with 
                           Some (Robot r) -> r 
                           | _ -> raise(Failure("Error: Not find Robot"))
@@ -435,7 +442,7 @@ let get_robot (Description(d', _) : description) : field list =
     @return [string list] *)
 let get_activelyup (d : description) : string list = 
   match d with 
-  | Description(d', _) -> (match List.find_opt (fun x -> match x with ActivelyUpdate _ -> true | _-> false) d' with 
+  | Description(d', _,_) -> (match List.find_opt (fun x -> match x with ActivelyUpdate _ -> true | _-> false) d' with 
                           Some (ActivelyUpdate a) -> List.map string_of_valretr a
                           | _ -> raise(Failure("Error: Not find ActivelyUpdate")))
 
diff --git a/lib/gencoq.ml b/lib/gencoq.ml
index 3abfb5fc5745bd3725a81510a3c3af5b5bab4666..8db81af4f49390d75dbadc16a1e2409b1e3fd6f0 100644
--- a/lib/gencoq.ml
+++ b/lib/gencoq.ml
@@ -153,12 +153,13 @@ let instance_R_R2 (s:space) (d: information list): stmt list =
     @param int n 
     @return [stmt list]*)
 let instance_ring (n:int) : stmt list =
-  if n > 0 then 
-  Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n);Raw("ring_size_spec:= (* QUOI METTRE ? *)")]))
-  :: Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))
-  ::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
+  let ring = if n > 0 then 
+  Instance("MyRing",Raw("RingSpec"),Record([Raw("ring_size := "^string_of_int n);Raw("ring_size_spec:= ltac:(auto)")]))
+  
   else
-    RawCoq(["Context {RR : RingSpec}."])::[]
+    RawCoq(["Context {RR : RingSpec}."])
+  in
+  ring::Notation("ring_node",App(Cst "finite_node",[Cst "ring_size"] ))::Instance("Loc",Cst "Location",App(Cst "make_Location",[Cst "ring_node"]))::[]
 
 (**[instance_space s] retourne une liste de stmt permettant de generer le code coq pour instancier l'espace s
         @param space  [s] à instancier pour le moment seulement R, R2, Ring
@@ -178,11 +179,20 @@ let instance_space (s: space) (d : information list): stmt list =
   @param string valeur de retour du robogram
   @return stmt 
     *)
-let instance_updfunc_rigid (valret : string) :stmt  =
+let instance_updfunc_rigid (valret : string) (d: information list):stmt list =
+  if not(get_space d = "Ring") then
   Instance("UpdateFunc",Raw("update_function ("^valret^") (Similarity.similarity "^valret^") unit"),Raw("{update := fun _ _ _ target _ => target;update_compat := ltac:(now repeat intro) }"))
-
-let instance_updfunc_Flexible (d:expr) (valret : string) : stmt =
+  ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])::[]
+  else 
+    Instance("FrameChoice",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);
+      frame_choice_Setoid := eq_setoid _ }"))::
+    Instance("UpdateFunc",Raw("update_function direction (Z * bool) unit"),Raw("{
+      update := fun config g _ dir _ => move_along (config (Good g)) dir;
+      update_compat := ltac:(repeat intro; subst; now apply move_along_compat) }"))::[]
+let instance_updfunc_Flexible (d:expr) (valret : string): stmt list =
   Instance("UpdateFunc",Raw("update_function (path "^valret^") (Similarity.similarity "^valret^") ratio"),Raw("  FlexibleUpdate "^string_of_expression d))
+  ::[]
 
 
 (**[instance_rigidity r valret] retourne une liste de stmt permettant de generer le code coq pour instancier la rigidite des deplacements 
@@ -190,18 +200,16 @@ let instance_updfunc_Flexible (d:expr) (valret : string) : stmt =
         @param valret valeur de retour du robogram 
         @return [stmt list]
           *)
-let instance_rigidity (r:rigidity) (valret : string) : stmt list =
+let instance_rigidity (r:rigidity) (valret : string) (world: information list): stmt list =
   match r with(*TODO: Est-ce la bonne maniere d'ecrire l'UpdateFunc?*)
   | Rigide ->     Instance("RobotChoice",Raw("robot_choice "^ valret),Raw("{ robot_choice_Setoid := "^valret^"_Setoid}")) 
                   ::Instance("ActiveChoice",App(Var(0,"update_choice"),[Var(0,"unit")]),Raw("NoChoice"))
-                  :: instance_updfunc_rigid valret
-                  ::RawCoq(["Instance Rigid : RigidSetting.";"Proof using . split. reflexivity. Qed."])
-                  ::[]
+                  :: instance_updfunc_rigid valret world
+                  
   | Flexible d -> Instance("RobotChoice",Raw("robot_choice (path "^ valret^")"),Raw("{ robot_choice_Setoid := path_Setoid "^valret^"}")) 
                   ::Instance("ActiveChoice",App(Var(0,"update_choice"),[Var(0,"ratio")]),Raw "Flexible.OnlyFlexible")
                   ::Var(string_of_expression d,Raw("R"))
                   ::instance_updfunc_Flexible d valret 
-                  ::[]
     
 
 (**[instance_info fl] retourne une liste de stmt permettant de generer le code coq pour instancier de l'état du robot
@@ -274,7 +282,7 @@ let require_space (s: space) : stmt =
   match s with  
   | R -> Require(true,["Pactole.Spaces.R"])
   | R2 -> Require(true,["Pactole.Spaces.R2";"Rbase"])
-  | ZnZ _ ->  Require(true,["Pactole.Spaces.Ring"]) 
+  | ZnZ _ ->  Require(true,["Pactole.Spaces.Ring";"Reals";"Pactole.Spaces.Isomorphism"]) 
   | _ ->raise(Failure ("Not implemanted")) 
 
 (**[require_multi s] retourne un stmt permettant de generer le require pour la multiplicité 
@@ -318,7 +326,7 @@ let valret = get_val_ret world in
   | [] -> []
   | h::t-> (match h with 
           | Space s -> newline::(instance_space s world) @ genworld t
-          | Rigidity r -> genworld t @newline::(instance_rigidity r valret) 
+          | Rigidity r -> genworld t @newline::(instance_rigidity r valret world) 
           | Robot r -> newline::(instance_info r) @ genworld t
           | Sync s -> genworld t @(instance_sync s) 
           | Sensors s -> genworld t @ (instance_sensors s)
@@ -342,11 +350,23 @@ let generate_robogram (r : expr list) (d: information list) : stmt list =
                      ::[]
   | [] ->  Def ("Robogram_pgm (s : observation)",Raw(valretcoq),Raw("[]")) ::[]
 
-let generate (Description(d,r) : description) (section_name : string)=
-  if Ast.check_light (Description (d,r)) then
+let rec n_times (x : int) :string =
+  if x > 0 then n_times (x -1)^"*"^"nat"
+  else "nat"
+  
+let generate_measure (Measure(i,_): measure) : stmt list = 
+  let ret = String.concat "*"(List.init i (fun _ ->"nat")) in
+  let to_change = String.concat ","(List.init i (fun _ ->"0%nat"))in
+  RawCoq(["Function measure (s : observation) : "^ret ^" := 
+            (*A REMPLIR GRACE AU GRAPH*)
+            ("^to_change^")."; (*TODO: à modifié pour utiliser le graph*)
+          "Instance measure_compat : Proper (equiv ==> Logic.eq) measure."])::proof_to_complete
+
+let generate (Description(d,r,m) : description) (section_name : string)=
+  if Ast.check_light (Description (d,r,m)) then
     let file_out = open_out ("./generate/"^section_name^".v") in 
     let format_file = Format.formatter_of_out_channel file_out in
-    let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d) in
+    let section = Section(section_name,(generate_instances d)@newline::generate_robogram r d@newline::generate_measure m) in
     Format.fprintf format_file "%a@." Coq.pretty_l ((generate_requires d)@[section]);
     close_out file_out
   else 
diff --git a/lib/lexer.mll b/lib/lexer.mll
index 6215f7015058cc27a1f139e6fa3c2e5fda1343ba..e9329f511e318bd35a9e668c11ae969dcc952a3b 100644
--- a/lib/lexer.mll
+++ b/lib/lexer.mll
@@ -14,6 +14,7 @@ let keyword = ['A'-'Z']alpha+
 rule token = parse 
     | "World"           {WORLD}
     | "Robogram"        {ROBOGRAM}
+    | "Measure"         {MEASURE}
     | "Sync"            {SYNC}
     | "FSYNC"           {FSYNC}
     | "SSYNC"           {SSYNC}
@@ -102,6 +103,7 @@ rule token = parse
     | "/*"              {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; comment lexbuf}
     | integer           {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; INT (int_of_string (Lexing.lexeme lexbuf))}
     | float             {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; FLOAT (float_of_string(Lexing.lexeme lexbuf) )}
+    | ","               {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; COMMA}
     | keyword           {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; KEYWORD (Lexing.lexeme lexbuf)}
     | variable          {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; VARIABLE (Lexing.lexeme lexbuf)}
     | space             {numero_carac := !numero_carac + (String.length (Lexing.lexeme lexbuf)) ; token lexbuf}
diff --git a/lib/parser.mly b/lib/parser.mly
index ccfc79ca862b3ff9fe8002bd7c7dfbd41d1267e5..c4fddcf7261b2b9147419580a894b310d11d048a 100644
--- a/lib/parser.mly
+++ b/lib/parser.mly
@@ -17,11 +17,12 @@
 /*%token MEMOIRE OBLIVIOUS FINITE INFINITE*/
 %token SHARE FULLCOMPASS CHIRALITY ONEAXEORIEN 
 %token RIGIDITY RIGIDE FLEXIBLE 
-%token COLON BRACKETOPEN BRACKETCLOSE SEMICOLON PARENOPEN PARENCLOSE 
+%token COLON BRACKETOPEN BRACKETCLOSE SEMICOLON PARENOPEN PARENCLOSE COMMA
 %token POINT
 %token ROBOT PUBLIC PRIVATE ACTIVELYUP
 %token ROLES
-%token WORLD ROBOGRAM 
+%token WORLD ROBOGRAM MEASURE
+
 
 %token LOCATION DIRECTION
 
@@ -49,7 +50,10 @@
 %%
 
 description : 
-    | WORLD COLON information* ROBOGRAM COLON robogram EOF {Description (List.flatten $3,$6)}
+    | WORLD COLON information* 
+      ROBOGRAM COLON robogram
+      MEASURE COLON measure
+      EOF {Description (List.flatten $3,$6,$9)}
 
 
 /* DESCRIPTION DE L'ENVIRONNEMENT*/
@@ -300,4 +304,9 @@ resultpattern :
 pattern :
     | v = VARIABLE {Var v}
     | v = VARIABLE COLON COLON e = pattern {Cons(Var v,e)}
-    | PARENOPEN s = set PARENCLOSE COLON COLON e = pattern {Cons(Set s,e)}
\ No newline at end of file
+    | PARENOPEN s = set PARENCLOSE COLON COLON e = pattern {Cons(Set s,e)}
+
+
+
+measure:
+| PARENOPEN l = separated_list(COMMA,VARIABLE) PARENCLOSE {Measure(List.length l, Graph"none")}
\ No newline at end of file