diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 704 |
1 files changed, 388 insertions, 316 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 0fed211d..3bf556f1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: constrintern.ml 13332 2010-07-26 22:12:43Z msozeau $ *) open Pp open Util @@ -28,7 +28,10 @@ open Inductiveops (* To interpret implicits and arg scopes of variables in inductive types and recursive definitions and of projection names in records *) -type var_internalization_type = Inductive | Recursive | Method +type var_internalization_type = + | Inductive of identifier list (* list of params *) + | Recursive + | Method type var_internalization_data = (* type of the "free" variable, for coqdoc, e.g. while typing the @@ -45,19 +48,12 @@ type var_internalization_data = type internalization_env = (identifier * var_internalization_data) list -type full_internalization_env = - (* a superset of the list of variables that may be automatically - inserted and that must not occur as binders *) - identifier list * - (* mapping of the variables to their internalization data *) - internalization_env - type raw_binder = (name * binding_kind * rawconstr option * rawconstr) let interning_grammar = ref false (* Historically for parsing grammar rules, but in fact used only for - translator, v7 parsing, and unstrict tactic internalisation *) + translator, v7 parsing, and unstrict tactic internalization *) let for_grammar f x = interning_grammar := true; let a = f x in @@ -92,9 +88,9 @@ let global_reference_in_absolute_module dir id = constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) (**********************************************************************) -(* Internalisation errors *) +(* Internalization errors *) -type internalisation_error = +type internalization_error = | VariableCapture of identifier | WrongExplicitImplicit | IllegalMetavariable @@ -104,7 +100,7 @@ type internalisation_error = | BadPatternsNumber of int * int | BadExplicitationNumber of explicitation * int option -exception InternalisationError of loc * internalisation_error +exception InternalizationError of loc * internalization_error let explain_variable_capture id = str "The variable " ++ pr_id id ++ str " occurs in its type" @@ -146,7 +142,7 @@ let explain_bad_explicitation_number n po = str "Bad explicitation name: found " ++ pr_id id ++ str" but was expecting " ++ s -let explain_internalisation_error e = +let explain_internalization_error e = let pp = match e with | VariableCapture id -> explain_variable_capture id | WrongExplicitImplicit -> explain_wrong_explicit_implicit @@ -171,30 +167,26 @@ let error_inductive_parameter_not_implicit loc = (* Pre-computing the implicit arguments and arguments scopes needed *) (* for interpretation *) -let empty_internalization_env = ([],[]) +let empty_internalization_env = [] -let set_internalization_env_params ienv params = - let nparams = List.length params in - if nparams = 0 then - ([],ienv) - else - let ienv_with_implicit_params = - List.map (fun (id,(ty,_,impl,scopes)) -> - let sub_impl,_ = list_chop nparams impl in - let sub_impl' = List.filter is_status_implicit sub_impl in - (id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in - (params, ienv_with_implicit_params) - -let compute_internalization_data env ty typ impls = - let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in - (ty, [], impl, compute_arguments_scope typ) - -let compute_full_internalization_env env ty params idl typl impll = - set_internalization_env_params - (list_map3 - (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) - idl typl impll) - params +let compute_explicitable_implicit imps = function + | Inductive params -> + (* In inductive types, the parameters are fixed implicit arguments *) + let sub_impl,_ = list_chop (List.length params) imps in + let sub_impl' = List.filter is_status_implicit sub_impl in + List.map name_of_implicit sub_impl' + | Recursive | Method -> + (* Unable to know in advance what the implicit arguments will be *) + [] + +let compute_internalization_data env ty typ impl = + let impl = compute_implicits_with_manual env typ (is_implicit_args()) impl in + let expls_impl = compute_explicitable_implicit impl ty in + (ty, expls_impl, impl, compute_arguments_scope typ) + +let compute_internalization_env env ty = + list_map3 + (fun id typ impl -> (id,compute_internalization_data env ty typ impl)) (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -216,18 +208,18 @@ let expand_notation_string ntn n = (* This contracts the special case of "{ _ }" for sumbool, sumor notations *) (* Remark: expansion of squash at definition is done in metasyntax.ml *) -let contract_notation ntn (l,ll) = +let contract_notation ntn (l,ll,bll) = let ntn' = ref ntn in let rec contract_squash n = function | [] -> [] - | CNotation (_,"{ _ }",([a],[])) :: l -> + | CNotation (_,"{ _ }",([a],[],[])) :: l -> ntn' := expand_notation_string !ntn' n; contract_squash n (a::l) | a :: l -> a::contract_squash (n+1) l in let l = contract_squash 0 l in (* side effect; don't inline *) - !ntn',(l,ll) + !ntn',(l,ll,bll) let contract_pat_notation ntn (l,ll) = let ntn' = ref ntn in @@ -250,43 +242,219 @@ let make_current_scope = function | (Some tmp_scope,scopes) -> tmp_scope::scopes | None,scopes -> scopes -let set_var_scope loc id (_,_,scopt,scopes) varscopes = - let idscopes = List.assoc id varscopes in - if !idscopes <> None & - make_current_scope (Option.get !idscopes) - <> make_current_scope (scopt,scopes) then - let pr_scope_stack = function - | [] -> str "the empty scope stack" - | [a] -> str "scope " ++ str a - | l -> str "scope stack " ++ - str "[" ++ prlist_with_sep pr_comma str l ++ str "]" in - user_err_loc (loc,"set_var_scope", - pr_id id ++ str " is used both in " ++ - pr_scope_stack (make_current_scope (Option.get !idscopes)) ++ - strbrk " and in " ++ - pr_scope_stack (make_current_scope (scopt,scopes))) - else - idscopes := Some (scopt,scopes) +let pr_scope_stack = function + | [] -> str "the empty scope stack" + | [a] -> str "scope " ++ str a + | l -> str "scope stack " ++ + str "[" ++ prlist_with_sep pr_comma str l ++ str "]" + +let error_inconsistent_scope loc id scopes1 scopes2 = + user_err_loc (loc,"set_var_scope", + pr_id id ++ str " is used both in " ++ + pr_scope_stack scopes1 ++ strbrk " and in " ++ pr_scope_stack scopes2) + +let error_expect_constr_notation_type loc id = + user_err_loc (loc,"", + pr_id id ++ str " is bound in the notation to a term variable.") + +let error_expect_binder_notation_type loc id = + user_err_loc (loc,"", + pr_id id ++ + str " is expected to occur in binding position in the right-hand side.") + +let set_var_scope loc id istermvar (_,_,scopt,scopes) ntnvars = + try + let idscopes,typ = List.assoc id ntnvars in + if !idscopes <> None & + make_current_scope (Option.get !idscopes) + <> make_current_scope (scopt,scopes) then + error_inconsistent_scope loc id + (make_current_scope (Option.get !idscopes)) + (make_current_scope (scopt,scopes)) + else + idscopes := Some (scopt,scopes); + match typ with + | NtnInternTypeBinder -> + if istermvar then error_expect_binder_notation_type loc id + | NtnInternTypeConstr -> + (* We need sometimes to parse idents at a constr level for + factorization and we cannot enforce this constraint: + if not istermvar then error_expect_constr_notation_type loc id *) + () + | NtnInternTypeIdent -> () + with Not_found -> + (* Not in a notation *) + () + +let set_type_scope (ids,unb,tmp_scope,scopes) = + (ids,unb,Some Notation.type_scope,scopes) + +let reset_tmp_scope (ids,unb,tmp_scope,scopes) = + (ids,unb,None,scopes) + +let rec it_mkRProd env body = + match env with + (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) + | [] -> body + +let rec it_mkRLambda env body = + match env with + (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) + | [] -> body + +(**********************************************************************) +(* Utilities for binders *) + +let check_capture loc ty = function + | Name id when occur_var_constr_expr id ty -> + raise (InternalizationError (loc,VariableCapture id)) + | _ -> + () + +let locate_if_isevar loc na = function + | RHole _ -> + (try match na with + | Name id -> Reserve.find_reserved_type id + | Anonymous -> raise Not_found + with Not_found -> RHole (loc, Evd.BinderType na)) + | x -> x + +let check_hidden_implicit_parameters id (_,_,_,impls) = + if List.exists (function + | (_,(Inductive indparams,_,_,_)) -> List.mem id indparams + | _ -> false) impls + then + errorlabstrm "" (strbrk "A parameter of an inductive type " ++ + pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") + +let push_name_env ?(global_level=false) lvar (ids,unb,tmpsc,scopes as env) = + function + | loc,Anonymous -> + if global_level then + user_err_loc (loc,"", str "Anonymous variables not allowed"); + env + | loc,Name id -> + check_hidden_implicit_parameters id lvar; + set_var_scope loc id false env (let (_,_,ntnvars,_) = lvar in ntnvars); + if global_level then Dumpglob.dump_definition (loc,id) true "var" + else Dumpglob.dump_binding loc id; + (Idset.add id ids,unb,tmpsc,scopes) + +let intern_generalized_binder ?(global_level=false) intern_type lvar + (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = + let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in + let ty, ids' = + if t then ty, ids else + Implicit_quantifiers.implicit_application ids + Implicit_quantifiers.combine_params_freevar ty + in + let ty' = intern_type (ids,true,tmpsc,sc) ty in + let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in + let env' = List.fold_left (fun env (x, l) -> push_name_env ~global_level lvar env (l, Name x)) env fvs in + let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in + let na = match na with + | Anonymous -> + if global_level then na + else + let name = + let id = + match ty with + | CApp (_, (_, CRef (Ident (loc,id))), _) -> id + | _ -> id_of_string "H" + in Implicit_quantifiers.make_fresh ids' (Global.env ()) id + in Name name + | _ -> na + in (push_name_env ~global_level lvar env' (loc,na)), (na,b',None,ty') :: List.rev bl + +let intern_local_binder_aux ?(global_level=false) intern intern_type lvar (env,bl) = function + | LocalRawAssum(nal,bk,ty) -> + (match bk with + | Default k -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = locate_if_isevar loc na (intern_type env ty) in + List.fold_left + (fun (env,bl) na -> + (push_name_env lvar env na,(snd na,k,None,ty)::bl)) + (env,bl) nal + | Generalized (b,b',t) -> + let env, b = intern_generalized_binder ~global_level intern_type lvar env bl (List.hd nal) b b' t ty in + env, b @ bl) + | LocalRawDef((loc,na as locna),def) -> + (push_name_env lvar env locna, + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) + +let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = + let c = intern (ids,true,tmp_scope,scopes) c in + let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in + let env', c' = + let abs = + let pi = + match ak with + | Some AbsPi -> true + | None when tmp_scope = Some Notation.type_scope + || List.mem Notation.type_scope scopes -> true + | _ -> false + in + if pi then + (fun (id, loc') acc -> + RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + else + (fun (id, loc') acc -> + RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) + in + List.fold_right (fun (id, loc as lid) (env, acc) -> + let env' = push_name_env lvar env (loc, Name id) in + (env', abs lid acc)) fvs (env,c) + in c' + +let iterate_binder intern lvar (env,bl) = function + | LocalRawAssum(nal,bk,ty) -> + let intern_type env = intern (set_type_scope env) in + (match bk with + | Default k -> + let (loc,na) = List.hd nal in + (* TODO: fail if several names with different implicit types *) + let ty = intern_type env ty in + let ty = locate_if_isevar loc na ty in + List.fold_left + (fun (env,bl) na -> (push_name_env lvar env na,(snd na,k,None,ty)::bl)) + (env,bl) nal + | Generalized (b,b',t) -> + let env, b = intern_generalized_binder intern_type lvar env bl (List.hd nal) b b' t ty in + env, b @ bl) + | LocalRawDef((loc,na as locna),def) -> + (push_name_env lvar env locna, + (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) (**********************************************************************) (* Syntax extensions *) -let traverse_binder (subst,substlist) (renaming,(ids,unb,tmpsc,scopes as env))= +let option_mem_assoc id = function + | Some (id',c) -> id = id' + | None -> false + +let find_fresh_name renaming (terms,termlists,binders) id = + let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) terms in + let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) termlists) in + let fvs3 = List.map snd renaming in + (* TODO binders *) + let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in + next_ident_away id fvs + +let traverse_binder (terms,_,_ as subst) + (renaming,(ids,unb,tmpsc,scopes as env))= function | Anonymous -> (renaming,env),Anonymous | Name id -> try (* Binders bound in the notation are considered first-order objects *) - let _,na = coerce_to_name (fst (List.assoc id subst)) in + let _,na = coerce_to_name (fst (List.assoc id terms)) in (renaming,(name_fold Idset.add na ids,unb,tmpsc,scopes)), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) - let fvs1 = List.map (fun (_,(c,_)) -> free_vars_of_constr_expr c) subst in - let fvs2 = List.flatten (List.map (fun (_,(l,_)) -> List.map free_vars_of_constr_expr l) substlist) in - let fvs3 = List.map snd renaming in - let fvs = List.flatten (List.map Idset.elements (fvs1@fvs2)) @ fvs3 in - let id' = next_ident_away id fvs in + let id' = find_fresh_name renaming subst id in let renaming' = if id=id' then renaming else (id,id')::renaming in (renaming',env), Name id' @@ -294,17 +462,18 @@ let rec subst_iterator y t = function | RVar (_,id) as x -> if id = y then t else x | x -> map_rawconstr (subst_iterator y t) x -let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c = - let (renaming,(ids,unb,_,scopes)) = infos in - let subinfos = renaming,(ids,unb,None,scopes) in - match c with - | AVar id -> +let subst_aconstr_in_rawconstr loc intern lvar subst infos c = + let (terms,termlists,binders) = subst in + let rec aux (terms,binderopt as subst') (renaming,(ids,unb,_,scopes as env)) c = + let subinfos = renaming,(ids,unb,None,scopes) in + match c with + | AVar id -> begin (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try - let (a,(scopt,subscopes)) = List.assoc id subst in - interp (ids,unb,scopt,subscopes@scopes) a + let (a,(scopt,subscopes)) = List.assoc id terms in + intern (ids,unb,scopt,subscopes@scopes) a with Not_found -> try RVar (loc,List.assoc id renaming) @@ -312,83 +481,96 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c = (* Happens for local notation joint with inductive/fixpoint defs *) RVar (loc,id) end - | AList (x,_,iter,terminator,lassoc) -> + | AList (x,_,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) - let (l,(scopt,subscopes)) = List.assoc x substlist in - let termin = - subst_aconstr_in_rawconstr loc interp sub subinfos terminator in + let (l,(scopt,subscopes)) = List.assoc x termlists in + let termin = aux subst' subinfos terminator in List.fold_right (fun a t -> subst_iterator ldots_var t - (subst_aconstr_in_rawconstr loc interp - ((x,(a,(scopt,subscopes)))::subst,substlist) subinfos iter)) + (aux ((x,(a,(scopt,subscopes)))::terms,binderopt) subinfos iter)) (if lassoc then List.rev l else l) termin with Not_found -> anomaly "Inconsistent substitution of recursive notation") - | AHole (Evd.BinderType (Name id as na)) -> + | AHole (Evd.BinderType (Name id as na)) -> let na = - try snd (coerce_to_name (fst (List.assoc id subst))) + try snd (coerce_to_name (fst (List.assoc id terms))) with Not_found -> na in RHole (loc,Evd.BinderType na) - | t -> - rawconstr_of_aconstr_with_binders loc (traverse_binder sub) - (subst_aconstr_in_rawconstr loc interp sub) subinfos t - -let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs = - let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in - let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in + | ABinderList (x,_,iter,terminator) -> + (try + (* All elements of the list are in scopes (scopt,subscopes) *) + let (bl,(scopt,subscopes)) = List.assoc x binders in + let env,bl = List.fold_left (iterate_binder intern lvar) (env,[]) bl in + let termin = aux subst' (renaming,env) terminator in + List.fold_left (fun t binder -> + subst_iterator ldots_var t + (aux (terms,Some(x,binder)) subinfos iter)) + termin bl + with Not_found -> + anomaly "Inconsistent substitution of recursive notation") + | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt -> + let (na,bk,_,t) = snd (Option.get binderopt) in + RProd (loc,na,bk,t,aux subst' infos c') + | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt -> + let (na,bk,_,t) = snd (Option.get binderopt) in + RLambda (loc,na,bk,t,aux subst' infos c') + | t -> + rawconstr_of_aconstr_with_binders loc (traverse_binder subst) + (aux subst') subinfos t + in aux (terms,None) infos c + +let split_by_type ids = + List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> + match typ with + | NtnTypeConstr -> ((x,scl)::l1,l2,l3) + | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) + | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) + +let make_subst ids l = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids l + +let intern_notation intern (_,_,tmp_scope,scopes as env) lvar loc ntn fullargs = + let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in + let ((ids,c),df) = interp_notation loc ntn (tmp_scope,scopes) in Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df; - let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in - let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in - subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c - -let set_type_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,Some Notation.type_scope,scopes) - -let reset_tmp_scope (ids,unb,tmp_scope,scopes) = - (ids,unb,None,scopes) - -let rec it_mkRProd env body = - match env with - (na, bk, _, t) :: tl -> it_mkRProd tl (RProd (dummy_loc, na, bk, t, body)) - | [] -> body - -let rec it_mkRLambda env body = - match env with - (na, bk, _, t) :: tl -> it_mkRLambda tl (RLambda (dummy_loc, na, bk, t, body)) - | [] -> body + let ids,idsl,idsbl = split_by_type ids in + let terms = make_subst ids args in + let termlists = make_subst idsl argslist in + let binders = make_subst idsbl bll in + subst_aconstr_in_rawconstr loc intern lvar + (terms,termlists,binders) ([],env) c (**********************************************************************) (* Discriminating between bound variables and global references *) -(* [vars1] is a set of name to avoid (used for the tactic language); - [vars2] is the set of global variables, env is the set of variables - abstracted until this point *) - let string_of_ty = function - | Inductive -> "ind" + | Inductive _ -> "ind" | Recursive -> "def" | Method -> "meth" -let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) loc id = - let (vars1,unbndltacvars) = ltacvars in +let intern_var (ids,_,_,_ as genv) (ltacvars,namedctxvars,ntnvars,impls) loc id = + let (ltacvars,unbndltacvars) = ltacvars in (* Is [id] an inductive type potentially with implicit *) try - let ty,l,impl,argsc = List.assoc id impls in - let l = List.map - (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in + let ty,expl_impls,impls,argsc = List.assoc id impls in + let expl_impls = List.map + (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in - Dumpglob.dump_reference loc "<>" (string_of_id id) tys; - RVar (loc,id), impl, argsc, l + Dumpglob.dump_reference loc "<>" (string_of_id id) tys; + RVar (loc,id), impls, argsc, expl_impls with Not_found -> - (* Is [id] bound in current env or is an ltac var bound to constr *) - if Idset.mem id env or List.mem id vars1 + (* Is [id] bound in current term or is an ltac var bound to constr *) + if Idset.mem id ids or List.mem id ltacvars then RVar (loc,id), [], [], [] (* Is [id] a notation variable *) - else if List.mem_assoc id vars3 + else if List.mem_assoc id ntnvars + then + (set_var_scope loc id true genv ntnvars; RVar (loc,id), [], [], []) + (* Is [id] the special variable for recursive notations *) + else if ntnvars <> [] && id = ldots_var then - (set_var_scope loc id genv vars3; RVar (loc,id), [], [], []) + RVar (loc,id), [], [], [] else (* Is [id] bound to a free name in ltac (this is an ltac error message) *) try @@ -398,7 +580,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0 with Not_found -> (* Is [id] a goal or section variable *) - let _ = Sign.lookup_named id vars2 in + let _ = Sign.lookup_named id namedctxvars in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) @@ -443,7 +625,7 @@ let intern_reference ref = (intern_extended_global_of_qualid (qualid_of_reference ref)) (* Is it a global reference or a syntactic definition? *) -let intern_qualid loc qid intern env args = +let intern_qualid loc qid intern env lvar args = match intern_extended_global_of_qualid (loc,qid) with | TrueGlobal ref -> RRef (loc, ref), args @@ -453,25 +635,25 @@ let intern_qualid loc qid intern env args = if List.length args < nids then error_not_enough_arguments loc; let args1,args2 = list_chop nids args in check_no_explicitation args1; - let subst = List.map2 (fun (id,scl) a -> (id,(fst a,scl))) ids args1 in - subst_aconstr_in_rawconstr loc intern (subst,[]) ([],env) c, args2 + let subst = make_subst ids (List.map fst args1) in + subst_aconstr_in_rawconstr loc intern lvar (subst,[],[]) ([],env) c, args2 (* Rule out section vars since these should have been found by intern_var *) -let intern_non_secvar_qualid loc qid intern env args = - match intern_qualid loc qid intern env args with +let intern_non_secvar_qualid loc qid intern env lvar args = + match intern_qualid loc qid intern env lvar args with | RRef (loc, VarRef id),_ -> error_global_not_found_loc loc qid | r -> r let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function | Qualid (loc, qid) -> - let r,args2 = intern_qualid loc qid intern env args in + let r,args2 = intern_qualid loc qid intern env lvar args in find_appl_head_data r, args2 | Ident (loc, id) -> try intern_var env lvar loc id, args with Not_found -> let qid = qualid_of_ident id in try - let r,args2 = intern_non_secvar_qualid loc qid intern env args in + let r,args2 = intern_non_secvar_qualid loc qid intern env lvar args in find_appl_head_data r, args2 with e -> (* Extra allowance for non globalizing functions *) @@ -482,7 +664,7 @@ let intern_applied_reference intern (_, unb, _, _ as env) lvar args = function let interp_reference vars r = let (r,_,_,_),_ = intern_applied_reference (fun _ -> error_not_enough_arguments dummy_loc) - (Idset.empty,false,None,[]) (vars,[],[],([],[])) [] r + (Idset.empty,false,None,[]) (vars,[],[],[]) [] r in r let apply_scope_env (ids,unb,_,scopes) = function @@ -529,14 +711,14 @@ let loc_of_lhs lhs = let check_linearity lhs ids = match has_duplicate ids with | Some id -> - raise (InternalisationError (loc_of_lhs lhs,NonLinearPattern id)) + raise (InternalizationError (loc_of_lhs lhs,NonLinearPattern id)) | None -> () (* Match the number of pattern against the number of matched args *) let check_number_of_pattern loc n l = let p = List.length l in - if n<>p then raise (InternalisationError (loc,BadPatternsNumber (n,p))) + if n<>p then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = if List.exists (fun ids' -> not (list_eq_set ids ids')) idsl then @@ -646,7 +828,7 @@ let find_constructor ref f aliases pats scopes = let (loc,qid) = qualid_of_reference ref in let gref = try locate_extended qid - with Not_found -> raise (InternalisationError (loc,NotAConstructor ref)) in + with Not_found -> raise (InternalizationError (loc,NotAConstructor ref)) in match gref with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in @@ -677,7 +859,7 @@ let find_constructor ref f aliases pats scopes = let find_pattern_variable = function | Ident (loc,id) -> id - | Qualid (loc,_) as x -> raise (InternalisationError(loc,NotAConstructor x)) + | Qualid (loc,_) as x -> raise (InternalizationError(loc,NotAConstructor x)) let maybe_constructor ref f aliases scopes = try @@ -686,7 +868,7 @@ let maybe_constructor ref f aliases scopes = ConstrPat (c,idspl1) with (* patt var does not exists globally *) - | InternalisationError _ -> VarPat (find_pattern_variable ref) + | InternalizationError _ -> VarPat (find_pattern_variable ref) (* patt var also exists globally but does not satisfy preconditions *) | (Environ.NotEvaluableConst _ | Not_found) -> if_verbose msg_warning (str "pattern " ++ pr_reference ref ++ @@ -696,7 +878,7 @@ let maybe_constructor ref f aliases scopes = let mustbe_constructor loc ref f aliases patl scopes = try find_constructor ref f aliases patl scopes with (Environ.NotEvaluableConst _ | Not_found) -> - raise (InternalisationError (loc,NotAConstructor ref)) + raise (InternalizationError (loc,NotAConstructor ref)) let sort_fields mode loc l completer = (*mode=false if pattern and true if constructor*) @@ -813,7 +995,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= intern_pat scopes aliases tmp_scope a | CPatNotation (loc, ntn, fullargs) -> let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in - let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + let ((ids',c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in + let (ids',idsl',_) = split_by_type ids' in Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df; let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in @@ -849,116 +1032,6 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat= (ids,List.flatten pl') (**********************************************************************) -(* Fix and CoFix *) - -(**********************************************************************) -(* Utilities for binders *) - -let check_capture loc ty = function - | Name id when occur_var_constr_expr id ty -> - raise (InternalisationError (loc,VariableCapture id)) - | _ -> - () - -let locate_if_isevar loc na = function - | RHole _ -> - (try match na with - | Name id -> Reserve.find_reserved_type id - | Anonymous -> raise Not_found - with Not_found -> RHole (loc, Evd.BinderType na)) - | x -> x - -let check_hidden_implicit_parameters id (_,_,_,(indnames,_)) = - if List.mem id indnames then - errorlabstrm "" (strbrk "A parameter or name of an inductive type " ++ - pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") - -let push_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) = function - | Anonymous -> - if fail_anonymous then errorlabstrm "" (str "Anonymous variables not allowed"); - env - | Name id -> - check_hidden_implicit_parameters id lvar; - (Idset.add id ids, unb,tmpsc,scopes) - -let push_loc_name_env ?(fail_anonymous=false) lvar (ids,unb,tmpsc,scopes as env) loc = function - | Anonymous -> - if fail_anonymous then user_err_loc (loc,"", str "Anonymous variables not allowed"); - env - | Name id -> - check_hidden_implicit_parameters id lvar; - Dumpglob.dump_binding loc id; - (Idset.add id ids,unb,tmpsc,scopes) - -let intern_generalized_binder ?(fail_anonymous=false) intern_type lvar - (ids,unb,tmpsc,sc as env) bl (loc, na) b b' t ty = - let ids = match na with Anonymous -> ids | Name na -> Idset.add na ids in - let ty, ids' = - if t then ty, ids else - Implicit_quantifiers.implicit_application ids - Implicit_quantifiers.combine_params_freevar ty - in - let ty' = intern_type (ids,true,tmpsc,sc) ty in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids ~allowed:ids' ty' in - let env' = List.fold_left (fun env (x, l) -> push_loc_name_env ~fail_anonymous lvar env l (Name x)) env fvs in - let bl = List.map (fun (id, loc) -> (Name id, b, None, RHole (loc, Evd.BinderType (Name id)))) fvs in - let na = match na with - | Anonymous -> - if fail_anonymous then na - else - let name = - let id = - match ty with - | CApp (_, (_, CRef (Ident (loc,id))), _) -> id - | _ -> id_of_string "H" - in Implicit_quantifiers.make_fresh ids' (Global.env ()) id - in Name name - | _ -> na - in (push_loc_name_env ~fail_anonymous lvar env' loc na), (na,b',None,ty') :: List.rev bl - -let intern_local_binder_aux ?(fail_anonymous=false) intern intern_type lvar ((ids,unb,ts,sc as env),bl) = function - | LocalRawAssum(nal,bk,ty) -> - (match bk with - | Default k -> - let (loc,na) = List.hd nal in - (* TODO: fail if several names with different implicit types *) - let ty = locate_if_isevar loc na (intern_type env ty) in - List.fold_left - (fun ((ids,unb,ts,sc),bl) (_,na) -> - ((name_fold Idset.add na ids,unb,ts,sc), (na,k,None,ty)::bl)) - (env,bl) nal - | Generalized (b,b',t) -> - let env, b = intern_generalized_binder ~fail_anonymous intern_type lvar env bl (List.hd nal) b b' t ty in - env, b @ bl) - | LocalRawDef((loc,na),def) -> - ((name_fold Idset.add na ids,unb,ts,sc), - (na,Explicit,Some(intern env def),RHole(loc,Evd.BinderType na))::bl) - -let intern_generalization intern (ids,unb,tmp_scope,scopes as env) lvar loc bk ak c = - let c = intern (ids,true,tmp_scope,scopes) c in - let fvs = Implicit_quantifiers.generalizable_vars_of_rawconstr ~bound:ids c in - let env', c' = - let abs = - let pi = - match ak with - | Some AbsPi -> true - | None when tmp_scope = Some Notation.type_scope - || List.mem Notation.type_scope scopes -> true - | _ -> false - in - if pi then - (fun (id, loc') acc -> - RProd (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) - else - (fun (id, loc') acc -> - RLambda (join_loc loc' loc, Name id, bk, RHole (loc', Evd.BinderType (Name id)), acc)) - in - List.fold_right (fun (id, loc as lid) (env, acc) -> - let env' = push_loc_name_env lvar env loc (Name id) in - (env', abs lid acc)) fvs (env,c) - in c' - -(**********************************************************************) (* Utilities for application *) let merge_impargs l args = @@ -1030,7 +1103,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalise sigma globalenv env allow_patvar lvar c = +let internalize sigma globalenv env allow_patvar lvar c = let rec intern (ids,unb,tmp_scope,scopes as env) = function | CRef ref as x -> let (c,imp,subscopes,l),_ = @@ -1044,17 +1117,16 @@ let internalise sigma globalenv env allow_patvar lvar c = let n = try list_index0 iddef lf with Not_found -> - raise (InternalisationError (locid,UnboundFixName (false,iddef))) + raise (InternalizationError (locid,UnboundFixName (false,iddef))) in let idl = Array.map (fun (id,(n,order),bl,ty,bd) -> let intern_ro_arg f = - let idx = Option.default 0 (index_of_annot bl n) in - let before, after = list_chop idx bl in + let before, after = split_at_annot bl n in let ((ids',_,_,_) as env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern (ids', unb, tmp_scope, scopes)) in - let n' = Option.map (fun _ -> List.length before) n in + let n' = Option.map (fun _ -> List.length rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, ((ids',_,_,_),rbl) = @@ -1082,7 +1154,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let n = try list_index0 iddef lf with Not_found -> - raise (InternalisationError (locid,UnboundFixName (true,iddef))) + raise (InternalizationError (locid,UnboundFixName (true,iddef))) in let idl = Array.map (fun (id,bl,ty,bd) -> @@ -1107,15 +1179,15 @@ let internalise sigma globalenv env allow_patvar lvar c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,(loc1,na),c1,c2) -> - RLetIn (loc, na, intern (reset_tmp_scope env) c1, - intern (push_loc_name_env lvar env loc1 na) c2) - | CNotation (loc,"- _",([CPrim (_,Numeral p)],[])) + | CLetIn (loc,na,c1,c2) -> + RLetIn (loc, snd na, intern (reset_tmp_scope env) c1, + intern (push_name_env lvar env na) c2) + | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> intern env (CPrim (loc,Numeral (Bigint.neg p))) - | CNotation (_,"( _ )",([a],[])) -> intern env a + | CNotation (_,"( _ )",([a],[],[])) -> intern env a | CNotation (loc,ntn,args) -> - intern_notation intern env loc ntn args + intern_notation intern env lvar loc ntn args | CGeneralization (loc,b,a,c) -> intern_generalization intern env lvar loc b a c | CPrim (loc, p) -> @@ -1138,8 +1210,8 @@ let internalise sigma globalenv env allow_patvar lvar c = let (c,impargs,args_scopes,l),args = match f with | CRef ref -> intern_applied_reference intern env lvar args ref - | CNotation (loc,ntn,([],[])) -> - let c = intern_notation intern env loc ntn ([],[]) in + | CNotation (loc,ntn,([],[],[])) -> + let c = intern_notation intern env lvar loc ntn ([],[],[]) in find_appl_head_data c, args | x -> (intern env f,[],[],[]), args in let args = @@ -1177,7 +1249,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let p' = Option.map (fun p -> let env'' = List.fold_left (push_name_env lvar) env ids in intern_type env'' p) po in - RLetTuple (loc, nal, (na', p'), b', + RLetTuple (loc, List.map snd nal, (na', p'), b', intern (List.fold_left (push_name_env lvar) env nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in @@ -1191,7 +1263,7 @@ let internalise sigma globalenv env allow_patvar lvar c = | CPatVar (loc, n) when allow_patvar -> RPatVar (loc, n) | CPatVar (loc, _) -> - raise (InternalisationError (loc,IllegalMetavariable)) + raise (InternalizationError (loc,IllegalMetavariable)) | CEvar (loc, n, l) -> REvar (loc, n, Option.map (List.map (intern env)) l) | CSort (loc, s) -> @@ -1252,27 +1324,27 @@ let internalise sigma globalenv env allow_patvar lvar c = if List.length l <> nindargs then error_wrong_numarg_inductive_loc loc globalenv ind nindargs; let nal = List.map (function - | RHole loc -> Anonymous - | RVar (_,id) -> Name id + | RHole (loc,_) -> loc,Anonymous + | RVar (loc,id) -> loc,Name id | c -> user_err_loc (loc_of_rawconstr c,"",str "Not a name.")) l in let parnal,realnal = list_chop nparams nal in - if List.exists ((<>) Anonymous) parnal then + if List.exists (fun (_,na) -> na <> Anonymous) parnal then error_inductive_parameter_not_implicit loc; - realnal, Some (loc,ind,nparams,realnal) + realnal, Some (loc,ind,nparams,List.map snd realnal) | None -> [], None in let na = match tm', na with - | RVar (_,id), None when Idset.mem id vars -> Name id - | RRef (loc, VarRef id), None -> Name id - | _, None -> Anonymous - | _, Some na -> na in - (tm',(na,typ)), na::ids + | RVar (loc,id), None when Idset.mem id vars -> loc,Name id + | RRef (loc, VarRef id), None -> loc,Name id + | _, None -> dummy_loc,Anonymous + | _, Some (loc,na) -> loc,na in + (tm',(snd na,typ)), na::ids and iterate_prod loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RProd (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern_type env body @@ -1280,24 +1352,22 @@ let internalise sigma globalenv env allow_patvar lvar c = match bk with | Default b -> default env b nal | Generalized (b,b',t) -> - let env, ibind = intern_generalized_binder intern_type lvar - env [] (List.hd nal) b b' t ty in + let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in let body = intern_type env body in it_mkRProd ibind body and iterate_lam loc2 env bk ty body nal = let rec default env bk = function - | (loc1,na)::nal -> + | (loc1,na as locna)::nal -> if nal <> [] then check_capture loc1 ty na; - let body = default (push_loc_name_env lvar env loc1 na) bk nal in + let body = default (push_name_env lvar env locna) bk nal in let ty = locate_if_isevar loc1 na (intern_type env ty) in RLambda (join_loc loc1 loc2, na, bk, ty, body) | [] -> intern env body in match bk with | Default b -> default env b nal | Generalized (b, b', t) -> - let env, ibind = intern_generalized_binder intern_type lvar - env [] (List.hd nal) b b' t ty in + let env, ibind = intern_generalized_binder intern_type lvar env [] (List.hd nal) b b' t ty in let body = intern env body in it_mkRLambda ibind body @@ -1345,9 +1415,9 @@ let internalise sigma globalenv env allow_patvar lvar c = try intern env c with - InternalisationError (loc,e) -> + InternalizationError (loc,e) -> user_err_loc (loc,"internalize", - explain_internalisation_error e) + explain_internalization_error e) (**************************************************************************) (* Functions to translate constr_expr into rawconstr *) @@ -1359,11 +1429,11 @@ let extract_ids env = Idset.empty let intern_gen isarity sigma env - ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let tmp_scope = if isarity then Some Notation.type_scope else None in - internalise sigma env (extract_ids env, false, tmp_scope,[]) + internalize sigma env (extract_ids env, false, tmp_scope,[]) allow_patvar (ltacvars,Environ.named_context env, [], impls) c let intern_constr sigma env c = intern_gen false sigma env c @@ -1374,8 +1444,8 @@ let intern_pattern env patt = try intern_cases_pattern env [] ([],[]) None patt with - InternalisationError (loc,e) -> - user_err_loc (loc,"internalize",explain_internalisation_error e) + InternalizationError (loc,e) -> + user_err_loc (loc,"internalize",explain_internalization_error e) type manual_implicits = (explicitation * (bool * bool * bool)) list @@ -1384,7 +1454,7 @@ type manual_implicits = (explicitation * (bool * bool * bool)) list (* Functions to parse and interpret constructions *) let interp_gen kind sigma env - ?(impls=([],[])) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c = intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars sigma env c in Default.understand_gen kind sigma env c @@ -1392,10 +1462,10 @@ let interp_gen kind sigma env let interp_constr sigma env c = interp_gen (OfType None) sigma env c -let interp_type sigma env ?(impls=([],[])) c = +let interp_type sigma env ?(impls=[]) c = interp_gen IsType sigma env ~impls c -let interp_casted_constr sigma env ?(impls=([],[])) c typ = +let interp_casted_constr sigma env ?(impls=[]) c typ = interp_gen (OfType (Some typ)) sigma env ~impls c let interp_open_constr sigma env c = @@ -1423,34 +1493,35 @@ let interp_constr_judgment sigma env c = Default.understand_judgment sigma env (intern_constr sigma env c) let interp_constr_evars_gen_impls ?evdref ?(fail_evar=true) - env ?(impls=([],[])) kind c = + env ?(impls=[]) kind c = let evdref = match evdref with | None -> ref Evd.empty | Some evdref -> evdref in - let c = intern_gen (kind=IsType) ~impls !evdref env c in - let imps = Implicit_quantifiers.implicits_of_rawterm c in + let istype = kind = IsType in + let c = intern_gen istype ~impls !evdref env c in + let imps = Implicit_quantifiers.implicits_of_rawterm ~with_products:istype c in Default.understand_tcc_evars ~fail_evar evdref env kind c, imps let interp_casted_constr_evars_impls ?evdref ?(fail_evar=true) - env ?(impls=([],[])) c typ = + env ?(impls=[]) c typ = interp_constr_evars_gen_impls ?evdref ~fail_evar env ~impls (OfType (Some typ)) c -let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c = +let interp_type_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env IsType ~impls c -let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=([],[])) c = +let interp_constr_evars_impls ?evdref ?(fail_evar=true) env ?(impls=[]) c = interp_constr_evars_gen_impls ?evdref ~fail_evar env (OfType None) ~impls c -let interp_constr_evars_gen evdref env ?(impls=([],[])) kind c = +let interp_constr_evars_gen evdref env ?(impls=[]) kind c = let c = intern_gen (kind=IsType) ~impls ( !evdref) env c in Default.understand_tcc_evars evdref env kind c -let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ = +let interp_casted_constr_evars evdref env ?(impls=[]) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c -let interp_type_evars evdref env ?(impls=([],[])) c = +let interp_type_evars evdref env ?(impls=[]) c = interp_constr_evars_gen evdref env IsType ~impls c type ltac_sign = identifier list * unbound_ltac_var_map @@ -1459,19 +1530,20 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c = let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in pattern_of_rawconstr c -let interp_aconstr ?(impls=([],[])) (vars,varslist) a = +let interp_aconstr ?(impls=[]) vars recvars a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in - let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, []) + let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in + let c = internalize Evd.empty (Global.env()) (extract_ids env, false, None, []) false (([],[]),Environ.named_context env,vl,impls) a in (* Translate and check that [c] has all its free variables bound in [vars] *) - let a = aconstr_of_rawconstr vars c in + let a = aconstr_of_rawconstr vars recvars c in + (* Splits variables into those that are binding, bound, or both *) + (* binding and bound *) + let out_scope = function None -> None,[] | Some (a,l) -> a,l in + let vars = List.map (fun (id,(sc,typ)) -> (id,(out_scope !sc,typ))) vl in (* Returns [a] and the ordered list of variables with their scopes *) - (* Variables occurring in binders have no relevant scope since bound *) - let vl = List.map (fun (id,r) -> - (id,match !r with None -> None,[] | Some (a,l) -> a,l)) vl in - list_chop (List.length vars) vl, a + vars, a (* Interpret binders and contexts *) @@ -1489,14 +1561,14 @@ open Environ open Term let my_intern_constr sigma env lvar acc c = - internalise sigma env acc false lvar c + internalize sigma env acc false lvar c let my_intern_type sigma env lvar acc c = my_intern_constr sigma env lvar (set_type_scope acc) c -let intern_context fail_anonymous sigma env params = - let lvar = (([],[]),Environ.named_context env, [], ([], [])) in +let intern_context global_level sigma env params = + let lvar = (([],[]),Environ.named_context env, [], []) in snd (List.fold_left - (intern_local_binder_aux ~fail_anonymous (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) + (intern_local_binder_aux ~global_level (my_intern_constr sigma env lvar) (my_intern_type sigma env lvar) lvar) ((extract_ids env,false,None,[]), []) params) let interp_rawcontext_gen understand_type understand_judgment env bl = @@ -1522,15 +1594,15 @@ let interp_rawcontext_gen understand_type understand_judgment env bl = (env,[],1,[]) (List.rev bl) in (env, par), impls -let interp_context_gen understand_type understand_judgment ?(fail_anonymous=false) sigma env params = - let bl = intern_context fail_anonymous sigma env params in +let interp_context_gen understand_type understand_judgment ?(global_level=false) sigma env params = + let bl = intern_context global_level sigma env params in interp_rawcontext_gen understand_type understand_judgment env bl -let interp_context ?(fail_anonymous=false) sigma env params = +let interp_context ?(global_level=false) sigma env params = interp_context_gen (Default.understand_type sigma) - (Default.understand_judgment sigma) ~fail_anonymous sigma env params + (Default.understand_judgment sigma) ~global_level sigma env params -let interp_context_evars ?(fail_anonymous=false) evdref env params = +let interp_context_evars ?(global_level=false) evdref env params = interp_context_gen (fun env t -> Default.understand_tcc_evars evdref env IsType t) - (Default.understand_judgment_tcc evdref) ~fail_anonymous !evdref env params + (Default.understand_judgment_tcc evdref) ~global_level !evdref env params |