diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:15:10 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-31 02:04:10 +0200 |
| commit | bf3b52f6a950490ad99b032cb0b41d32cff64824 (patch) | |
| tree | f880e1ce1989cd67c06c8a29284f35fc123bec09 /pretyping/pretyping.ml | |
| parent | 5dd98189c6554733fe4e22401e1637330cc8a30a (diff) | |
Using a more explicit algebraic type for evars of kind "MatchingVar".
A priori considered to be a good programming style.
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e72394fa2..0e152eaa6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -610,13 +610,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = (Retyping.get_judgment_of env.ExtraEnv.env !evdref c) in inh_conv_coerce_to_tycon ?loc env evdref j tycon - | GPatVar (someta,n) -> + | GPatVar kind -> let env = ltac_interp_name_env k0 lvar env !evdref in let ty = match tycon with | Some ty -> ty | None -> new_type_evar env evdref loc in - let k = Evar_kinds.MatchingVar (someta,n) in + let k = Evar_kinds.MatchingVar kind in { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> |