diff options
| -rw-r--r-- | interp/constrextern.ml | 33 |
1 files changed, 24 insertions, 9 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ffd598cd1a..006d9bc2f2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -583,18 +583,38 @@ let rec share_fix_binders n rbl ty def = | _ -> List.rev rbl, ty, def (**********************************************************************) +(* mapping rawterms to numerals (in presence of coercions, choose the *) +(* one with no delimiter if possible) *) + +let extern_possible_prim_token scopes r = + try + let (sc,n) = uninterp_prim_token r in + match availability_of_prim_token sc (make_current_scopes scopes) with + | None -> None + | Some key -> Some (insert_delimiters (CPrim (loc_of_rawconstr r,n)) key) + with No_match -> + None + +let extern_optimal_prim_token scopes r r' = + let c = extern_possible_prim_token scopes r in + let c' = if r==r' then None else extern_possible_prim_token scopes r' in + match c,c' with + | Some n, (Some (CDelimiters _) | None) | _, Some n -> n + | _ -> raise No_match + +(**********************************************************************) (* mapping rawterms to constr_expr *) let rec extern inctx scopes vars r = - let r = remove_coercions inctx r in + let r' = remove_coercions inctx r in try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_prim_token (loc_of_rawconstr r) scopes (uninterp_prim_token r) + extern_optimal_prim_token scopes r r' with No_match -> try if !Options.raw_print or !print_no_symbol then raise No_match; - extern_symbol scopes vars r (uninterp_notations r) - with No_match -> match r with + extern_symbol scopes vars r' (uninterp_notations r') + with No_match -> match r' with | RRef (loc,ref) -> extern_global loc (implicits_of_global ref) (extern_reference loc vars ref) @@ -763,11 +783,6 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,List.map (extern_cases_pattern_in_scope scopes vars) pl, extern inctx scopes vars c) -and extern_prim_token loc scopes (sc,p) = - match availability_of_prim_token sc (make_current_scopes scopes) with - | None -> raise No_match - | Some key -> insert_delimiters (CPrim (loc,p)) key - and extern_symbol (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match | (keyrule,pat,n as _rule)::rules -> |