label for WP

src/ide/gmain.ml

@@ -832,9 +832,11 @@ let scroll_to_source_goal g =
 	      current_file := f;
 	    end;
 	  move_to_line source_view (l-1)
-      | Ident.Fresh 
+      | Ident.Fresh -> 
+	  source_view#source_buffer#set_text "Fresh ident (no position available)\n";
+	  current_file := ""
       | Ident.Derived _ -> 
-	  source_view#source_buffer#set_text "(no position available)\n";
+	  source_view#source_buffer#set_text "Derived ident (no position available)\n";
 	  current_file := ""
   end
 

src/programs/pgm_wp.ml

@@ -382,7 +382,12 @@ let wp env e =
   wp_expr env e (default_post e.expr_type e.expr_effect)
 
 let add_wp_decl l f env =
-  let pr = create_prsymbol (id_fresh ("WP_" ^ l.ls_name.id_string)) in
+  let s = "WP_" ^ l.ls_name.id_string in
+  let id = match id_from_user l.ls_name with
+    | None -> id_fresh s
+    | Some loc -> id_user s loc
+  in
+  let pr = create_prsymbol id in
   let d = create_prop_decl Pgoal pr f in
   add_decl d env