diff options
| author | herbelin | 2012-01-20 21:08:39 +0000 |
|---|---|---|
| committer | herbelin | 2012-01-20 21:08:39 +0000 |
| commit | 6679d01256ce9a4a05c13eabbb4e2d85c3e6f075 (patch) | |
| tree | f7002c72a29516eb41a5e13f807754b999879039 /interp/constrintern.ml | |
| parent | 22a8453f551349bbafa14b914aa784693dcf3615 (diff) | |
Added new command "Set Parsing Explicit" for deactivating parsing (and
printing) of implicit arguments (a priori useful for teaching).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14928 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 11 |
1 files changed, 10 insertions, 1 deletions
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 |