aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r--pretyping/evarutil.ml24
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