diff options
| author | Emilio Jesus Gallego Arias | 2019-06-17 12:28:14 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-17 12:28:14 +0200 |
| commit | 5d18dfed8e68dd964bca5d64ca6bdd9f8ffbb1df (patch) | |
| tree | 705d949f1b8ac657d88d4a650d13ed3c7210e495 /interp/constrintern.ml | |
| parent | 6c53049049781a71e366edd738747f9b30eb5d94 (diff) | |
| parent | 1e3ca892b208c22956d6c8f89a1d5863711d0cd9 (diff) | |
Merge PR #10231: Adding location in warning telling implicit arguments differ in term and type
Reviewed-by: ejgallego
Ack-by: jashug
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 1a81dc41a1..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 - (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 |