diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 13 | ||||
| -rw-r--r-- | interp/constrextern.mli | 1 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 |
4 files changed, 15 insertions, 5 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index d5de74f8ab..537978269c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -44,11 +44,15 @@ let print_evar_arguments = ref false (* This governs printing of implicit arguments. When [print_implicits] is on then [print_implicits_explicit_args] tells how implicit args are printed. If on, implicit args are printed - prefixed by "!" otherwise the function and not the arguments is - prefixed by "!" *) + with the form (id:=arg) otherwise arguments are printed normally and + the function is prefixed by "@" *) let print_implicits = ref false let print_implicits_explicit_args = ref false +(* Tells if implicit arguments not known to be inferable from a rigid + position are systematically printed *) +let print_implicits_defensive = ref true + (* This forces printing of coercions *) let print_coercions = ref false @@ -503,8 +507,9 @@ let explicitize loc inctx impl (cf,f) args = let visible = !Options.raw_print or (!print_implicits & !print_implicits_explicit_args) or - (is_significant_implicit a impl tail & - (not (is_inferable_implicit inctx n imp))) + (!print_implicits_defensive & + is_significant_implicit a impl tail & + not (is_inferable_implicit inctx n imp)) in if visible then (a,Some (dummy_loc, ExplByName (name_of_implicit imp))) :: tail diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 9a9c55ec1d..a0f8661ccd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -45,6 +45,7 @@ val extern_sort : sorts -> rawsort (* Printing options *) val print_implicits : bool ref +val print_implicits_defensive : bool ref val print_arguments : bool ref val print_evar_arguments : bool ref val print_coercions : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 77e6ba42cf..9b3268930c 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 *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index edbf9fb62a..d7634d6e09 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -47,6 +47,8 @@ type full_implicits_env = identifier list * implicits_env type ltac_sign = identifier list * unbound_ltac_var_map +val insert_maximal_implicit : bool ref + (*s Internalisation performs interpretation of global names and notations *) val intern_constr : evar_map -> env -> constr_expr -> rawconstr |