diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 34 | ||||
| -rw-r--r-- | interp/impargs.ml | 9 |
2 files changed, 22 insertions, 21 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 838ef40545..70ce6cef19 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -716,20 +716,20 @@ let rec flatten_application c = match DAst.get c with (* one with no delimiter if possible) *) let extern_possible_prim_token (custom,scopes) r = - try - let (sc,n) = uninterp_prim_token r 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 -> None - | Some key -> Some (insert_coercion coercion (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim 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 + let (sc,n) = uninterp_prim_token r 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) + +let extern_possible extern r = + try Some (extern r) with No_match -> None + +let extern_optimal extern r r' = + let c = extern_possible extern r in + let c' = if r==r' then None else extern_possible extern r' in match c,c' with | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n | _ -> raise No_match @@ -769,12 +769,14 @@ let rec extern inctx scopes vars r = let r' = remove_coercions inctx r in try if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_optimal_prim_token scopes r r' + extern_optimal (extern_possible_prim_token scopes) r r' with No_match -> try let r'' = flatten_application r' in if !Flags.raw_print || !print_no_symbol then raise No_match; - extern_notation scopes vars r'' (uninterp_notations r'') + extern_optimal + (fun r -> extern_notation scopes vars r (uninterp_notations r)) + r r'' with No_match -> let loc = r'.CAst.loc in match DAst.get r' with diff --git a/interp/impargs.ml b/interp/impargs.ml index d8582d856e..d024a9e808 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -19,7 +19,6 @@ open Decl_kinds open Lib open Libobject open EConstr -open Termops open Reductionops open Constrexpr open Namegen @@ -200,16 +199,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc acc.(i) <- update pos rig acc.(i) | App (f,_) when rig && is_flexible_reference env sigma bound depth f -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Proj (p,c) when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Case _ when rig -> if strict then () else - iter_constr_with_full_binders sigma push_lift (frec false) ed c + iter_with_full_binders sigma push_lift (frec false) ed c | Evar _ -> () | _ -> - iter_constr_with_full_binders sigma push_lift (frec rig) ed c + iter_with_full_binders sigma push_lift (frec rig) ed c in let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in acc |