diff options
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 367544135..2da8e0f6f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -327,7 +327,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - if !Topconstr.oldfashion_patterns then + if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (loc, c, [], args) else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) @@ -358,7 +358,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2 + let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -374,7 +374,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns then l2 + let l2' = if !Topconstr.asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args |