diff options
| author | Maxime Dénès | 2018-03-09 23:08:55 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-09 23:08:55 +0100 |
| commit | 020c3448cc71618c3e74f64ae6217113072d1bbd (patch) | |
| tree | 0f4a7d4282730eb397c64be13ba10e14c465283a /interp/constrextern.ml | |
| parent | 1f2a922d52251f79a11d75c2205e6827a07e591b (diff) | |
| parent | 4d9375d18d58958d992f76799ad545b800321d78 (diff) | |
Merge PR #6949: Revert PR #873: New strategy based on open scopes for deciding…
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 949c7cbd8e..9efaff3b9f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -386,7 +386,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = try if !Flags.in_debugger || !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_pattern scopes vars pat - (uninterp_cases_pattern_notations scopes pat) + (uninterp_cases_pattern_notations pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -517,7 +517,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = try if !Flags.raw_print || !print_no_symbol then raise No_match; extern_notation_ind_pattern scopes vars ind args - (uninterp_ind_pattern_notations scopes ind) + (uninterp_ind_pattern_notations ind) with No_match -> let c = extern_reference vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -741,7 +741,7 @@ let rec extern inctx scopes vars r = 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 scopes r'') + extern_notation scopes vars r'' (uninterp_notations r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) |