diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 7 | ||||
| -rw-r--r-- | interp/constrintern.ml | 11 | ||||
| -rw-r--r-- | interp/constrintern.mli | 3 |
3 files changed, 18 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dc328ce75a..be60c9c307 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -479,6 +479,7 @@ let is_needed_for_correct_partial_application tail imp = (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) let explicitize loc inctx impl (cf,f) args = + let impl = if !Constrintern.parsing_explicit then [] else impl in let n = List.length args in let rec exprec q = function | a::args, imp::impl when is_status_implicit imp -> @@ -514,7 +515,9 @@ let explicitize loc inctx impl (cf,f) args = if args = [] then f else CApp (loc, (None, f), args) let extern_global loc impl f = - if impl <> [] & List.for_all is_status_implicit impl then + if not !Constrintern.parsing_explicit && + impl <> [] && List.for_all is_status_implicit impl + then CAppExpl (loc, (None, f), []) else CRef f @@ -523,7 +526,7 @@ let extern_app loc inctx impl (cf,f) args = if args = [] (* maybe caused by a hidden coercion *) then extern_global loc impl f else - if + if not !Constrintern.parsing_explicit && ((!Flags.raw_print or (!print_implicits & not !print_implicits_explicit_args)) & List.exists is_status_implicit impl) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7b0d4ff2b8..f36d56b83f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -166,6 +166,8 @@ let error_parameter_not_implicit loc = (* Pre-computing the implicit arguments and arguments scopes needed *) (* for interpretation *) +let parsing_explicit = ref false + let empty_internalization_env = Idmap.empty let compute_explicitable_implicit imps = function @@ -1215,6 +1217,7 @@ let internalize sigma globalenv env allow_patvar lvar c = | CRef ref as x -> let (c,imp,subscopes,l),_ = intern_applied_reference intern env (Environ.named_context globalenv) lvar [] ref in + assert (l=[]); (match intern_impargs c env imp subscopes l with | [] -> c | l -> GApp (constr_loc x, c, l)) @@ -1333,7 +1336,7 @@ let internalize sigma globalenv env allow_patvar lvar c = find_appl_head_data c, args | x -> (intern env f,[],[],[]), args in let args = - intern_impargs c env impargs args_scopes (merge_impargs l args) in + intern_impargs c env impargs args_scopes (merge_impargs l args) in check_projection isproj (List.length args) c; (match c with (* Now compact "(f args') args" *) @@ -1490,6 +1493,12 @@ let internalize sigma globalenv env allow_patvar lvar c = and intern_impargs c env l subscopes args = let l = select_impargs_size (List.length args) l in let eargs, rargs = extract_explicit_arg l args in + if !parsing_explicit then + if eargs <> [] then + error "Arguments given by name or position not supported in explicit mode." + else + intern_args env subscopes rargs + else let rec aux n impl subscopes eargs rargs = let (enva,subscopes') = apply_scope_env env subscopes in match (impl,rargs) with diff --git a/interp/constrintern.mli b/interp/constrintern.mli index be78837ff3..7d0009021d 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -178,5 +178,8 @@ val interp_aconstr : ?impls:internalization_env -> (identifier * identifier) list -> constr_expr -> (identifier * (subscopes * notation_var_internalization_type)) list * aconstr +(** Globalization options *) +val parsing_explicit : bool ref + (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b |