diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-11-21 13:58:08 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-11-21 13:58:08 +0100 |
| commit | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (patch) | |
| tree | 4d2bc9d39c1f6d7c4d00223143f18ae5bad500e5 /interp/constrextern.ml | |
| parent | 0e01de69c22a3793855b4c97c50e4514191b19bc (diff) | |
| parent | 094b577f61f105f0a92f3f84d7e739884dd993a7 (diff) | |
Merge PR #6185: [parser] Remove unnecessary statically initialized hook.
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0ce672cc8..e1df24f71 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -21,7 +21,6 @@ open CAst open Constrexpr open Constrexpr_ops open Notation_ops -open Topconstr open Glob_term open Glob_ops open Pattern @@ -414,7 +413,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.asymmetric_patterns then + if !asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (c, None, args) else CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), []) @@ -446,7 +445,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.asymmetric_patterns || not (List.is_empty ll) then l2 + let l2' = if !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 @@ -462,7 +461,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.asymmetric_patterns then l2 + let l2' = if !asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args |