diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 64bdb90a2..cebb45266 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -358,35 +358,35 @@ let new_pure_evar_full evd evi = let evd = Evd.add evd evk evi in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store typ = +let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let newevk = new_untyped_evar() in - let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store evd in + let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in (evd,newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store instance = +let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) instance = assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store typ in + let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ~naming typ in (evd,mkEvar (newevk,Array.of_list instance)) (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store typ = +let new_evar env evd ?src ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) typ = let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in let instance = match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?store instance + new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ~naming instance -let new_type_evar env evd ?src ?filter rigid = +let new_type_evar env evd ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = let evd', s = new_sort_variable rigid evd in - let evd', e = new_evar env evd' ?src ?filter (mkSort s) in + let evd', e = new_evar env evd' ?src ?filter ~naming (mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter rigid = - let evd', c = new_type_evar env !evdref ?src ?filter rigid in +let e_new_type_evar env evdref ?src ?filter ?(naming=Misctypes.IntroAnonymous) rigid = + let evd', c = new_type_evar env !evdref ?src ?filter ~naming rigid in evdref := evd'; c @@ -399,8 +399,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?(naming=Misctypes.IntroAnonymous) ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ~naming ty in evdref := evd'; ev |