The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Thu, 30 Aug 2012 20:34:45 +0200
AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> Le Thu, 30 Aug 2012 17:55:18 +0000,
> frank maltman 
> <frank.maltman AT googlemail.com>
>  a écrit :
> > 
> > Could someone please explain what's going on here?
> > 
> 
> Run the following to understand where your n0 comes from :
>
>   Definition insert_node_create_frequency
>     (c      : cache)
>     (n      : node)
>     (H_name : ~Name_Maps.In (node_name n) (cache_name_map c))
>     (H_freq : ~Node_Maps.In (node_frequency n) (cache_frequency_map c))
>   : insertion.
> 
> refine (match insert_maps_node (cache_frequency_map c) (cache_name_map
> c) n H_name H_freq with
>         | (exist node_m H_node_add, exist name_m H_name_add) =>
>           let ci := _ in
>           Insertion {|cache_frequency_map := node_m;
>                       cache_name_map := name_m;
>                       cache_invariant := ci|} n _
>         end).
> clear s s0.
> 
> (** Check the head of your goal, and you'll find your [n0] *)

I see, that makes sense. Thanks.