diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 77e6ba42c..9b3268930 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -44,6 +44,8 @@ let for_grammar f x = let variables_bind = ref false +let insert_maximal_implicit = ref false + (**********************************************************************) (* Internalisation errors *) @@ -1033,7 +1035,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let eargs' = List.remove_assoc id eargs in intern enva a :: aux (n+1) impl' subscopes' eargs' rargs with Not_found -> - if rargs=[] & eargs=[] & + if rargs=[] & eargs=[] & not !insert_maximal_implicit & not (List.for_all is_status_implicit impl') then (* Less regular arguments than expected: don't complete *) (* with implicit arguments *) |