diff options
Diffstat (limited to 'contrib/xml/cic2acic.ml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index c0bdf07a3..b3d164122 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -254,11 +254,11 @@ print_endline "PASSATO" ; flush stdout ; match g with Libnames.ConstructRef ((induri,_),_) | Libnames.IndRef (induri,_) -> - Nametab.sp_of_global None (Libnames.IndRef (induri,0)) + Nametab.sp_of_global (Libnames.IndRef (induri,0)) | Libnames.VarRef id -> (* Invariant: variables are never cooked in Coq *) raise Not_found - | _ -> Nametab.sp_of_global None g + | _ -> Nametab.sp_of_global g in Dischargedhypsmap.get_discharged_hyps sp, get_module_path_of_section_path sp |