diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 2 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
3 files changed, 7 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index fb5569e2e8..93cfdd9be2 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -308,8 +308,6 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr) [| u; p; cx; evar |]))) | None -> raise NoSubtacCoercion - (*evdref := Evd.add_conv_pb (Reduction.CONV, x, y) !evdref; - None*) in coerce_unify env x y let coerce_itf loc env evd v t c1 = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1972aee28b..b1dec0fd08 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -315,6 +315,11 @@ let push_rel_context_to_named_context env typ = let default_source = (Loc.ghost,Evar_kinds.InternalHole) +let new_pure_evar_full evd evi = + let evk = new_untyped_evar () in + let evd = Evd.add evd evk evi in + (evd, evk) + let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ = let newevk = new_untyped_evar() in let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7d917f15bd..0d482e9b03 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -36,6 +36,8 @@ val new_pure_evar : evar_map -> named_context_val -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> ?candidates:constr list -> types -> evar_map * evar +val new_pure_evar_full : evar_map -> evar_info -> evar_map * evar + (** the same with side-effects *) val e_new_evar : evar_map ref -> env -> ?src:Loc.t * Evar_kinds.t -> ?filter:bool list -> |