diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 37 |
1 files changed, 19 insertions, 18 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 7a14ca3e48..d5a5bde616 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -282,9 +282,9 @@ let insert_pat_alias ?loc p = function | Anonymous -> p | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) -let rec insert_coercion ?loc l c = match l with +let rec insert_entry_coercion ?loc l c = match l with | [] -> c - | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_coercion ?loc l c],[],[],[])) + | (inscope,ntn)::l -> CAst.make ?loc @@ CNotation (Some inscope,ntn,([insert_entry_coercion ?loc l c],[],[],[])) let rec insert_pat_coercion ?loc l c = match l with | [] -> c @@ -435,13 +435,10 @@ let extern_record_pattern cstrsp args = let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; - let (na,sc,p) = uninterp_prim_token_cases_pattern pat in + let (na,p,key) = uninterp_prim_token_cases_pattern pat scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - match availability_of_prim_token p sc scopes with - | None -> raise No_match - | Some key -> let loc = cases_pattern_loc pat in insert_pat_coercion ?loc coercion (insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na) @@ -453,7 +450,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> let loc = pat.CAst.loc in match DAst.get pat with - | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Name id) when entry_has_global custom || entry_has_ident custom -> + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) | pat -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -615,6 +613,10 @@ let is_projection nargs r = let is_hole = function CHole _ | CEvar _ -> true | _ -> false +let isCRef_no_univ = function + | CRef (_,None) -> true + | _ -> false + let is_significant_implicit a = not (is_hole (a.CAst.v)) @@ -843,13 +845,11 @@ let same_binder_type ty nal c = (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = - let (sc,n) = uninterp_prim_token r in + let (n,key) = uninterp_prim_token r scopes in match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match | Some coercion -> - match availability_of_prim_token n sc scopes with - | None -> raise No_match - | Some key -> insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) + insert_entry_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key) let filter_enough_applied nargs l = match nargs with @@ -931,7 +931,8 @@ let rec extern inctx ?impargs scopes vars r = match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) -> + CAst.make ?loc (extern_var ?loc id) | c -> @@ -1081,7 +1082,7 @@ let rec extern inctx ?impargs scopes vars r = | GFloat f -> extern_float f (snd scopes) - in insert_coercion coercion (CAst.make ?loc c) + in insert_entry_coercion coercion (CAst.make ?loc c) and extern_typ ?impargs (subentry,(_,scopes)) = extern true ?impargs (subentry,(Notation.current_type_scope_name (),scopes)) @@ -1279,14 +1280,11 @@ and extern_notation (custom,scopes as allscopes) vars t rules = pi3 (extern_local_binder (subentry,(scopt,scl@scopes')) vars bl)) binderlists in let c = make_notation loc specific_ntn (l,ll,bl,bll) in - let c = insert_coercion coercion (insert_delimiters c key) in + let c = insert_entry_coercion coercion (insert_delimiters c key) in let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args) | SynDefRule kn -> - match availability_of_entry_coercion custom InConstrEntrySomeLevel with - | None -> raise No_match - | Some coercion -> let l = List.map (fun (c,(subentry,(scopt,scl))) -> extern true (subentry,(scopt,scl@snd scopes)) vars c) @@ -1296,7 +1294,10 @@ and extern_notation (custom,scopes as allscopes) vars t rules = let args = fill_arg_scopes args argsscopes allscopes in let args = extern_args (extern true) vars args in let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in - insert_coercion coercion c + if isCRef_no_univ c.CAst.v && entry_has_global custom then c + else match availability_of_entry_coercion custom InConstrEntrySomeLevel with + | None -> raise No_match + | Some coercion -> insert_entry_coercion coercion c with No_match -> extern_notation allscopes vars t rules |