diff options
| author | Hugo Herbelin | 2019-05-25 19:21:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-16 14:04:19 +0200 |
| commit | e034b4090ca45410853db60ae2a5d2f220b48792 (patch) | |
| tree | c6f3476741850b4092c789f8bc9c8b3b2940b29d /interp/constrintern.ml | |
| parent | f95017c2c69ee258ae570b789bce696357d2c365 (diff) | |
Turning "manual_implicits" into a list of position in impargs.ml.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 622a9aee3d..e55f66e856 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2435,10 +2435,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let r = Retyping.relevance_of_type env sigma t in let d = LocalAssum (make_annot na r,t) in let impls = - if k == Implicit then - let na = match na with Name n -> Some n | Anonymous -> None in - CAst.make (ExplByPos (n, na), (true, true, true)) :: impls - else impls + if k == Implicit then CAst.make (Some (na,true)) :: impls + else CAst.make None :: impls in (push_rel d env, sigma, d::params, succ n, impls) | Some b -> @@ -2447,7 +2445,7 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) - in sigma, ((env, par), impls) + in sigma, ((env, par), List.rev impls) let interp_context_evars ?program_mode ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env sigma params = let int_env,bl = intern_context global_level env impl_env params in |