diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-05-02 16:04:50 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-02 16:04:50 +0200 |
| commit | 28accc370aa2f6fafbf50b69be7ae5dc06104212 (patch) | |
| tree | 7764de5a598390e9906f064170a480cfcfe0a38d /interp/constrintern.ml | |
| parent | 63503b99c46b27009e85e5c0fa9588b7424a589d (diff) | |
| parent | 9a48211ea8439a8502145e508b70ede9b5929b2f (diff) | |
Merge PR#582: Fix warnings
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 d75487ecf..3f99a3c7c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args = | Some _, GApp (loc, GRef (loc', ref, None), arg) -> GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> - user_err ~loc (str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance, its expanded head - does not start with a reference") + user_err ~loc (str "Notation " ++ pr_qualid qid + ++ str " cannot have a universe instance," + ++ str " its expanded head does not start with a reference") in c, projapp, args2 @@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t = let t' = locate_if_hole (loc_of_glob_constr t) na t in understand_tcc_evars env evdref ~expected_type:IsType t' -open Environ - let my_intern_constr env lvar acc c = internalize env acc false lvar c |