diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-08 17:12:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-27 19:31:49 +0100 |
| commit | e4a09fc480f512f54d5e7ba05d7e408dc5817a46 (patch) | |
| tree | 3ce040b7abb1860a3dc60aade92e454c121c355b /interp/constrextern.ml | |
| parent | 97960e114e72bc38814e78a71f06aca4fdfc4512 (diff) | |
Selecting which notation to print based on current stack of scope.
See discussion on coq-club starting on 23 August 2016.
An open question: what priority to give to "abbreviations"?
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 e1df24f71..bc8debd02 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -383,7 +383,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 pat) + (uninterp_cases_pattern_notations scopes pat) with No_match -> lift (fun ?loc -> function | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id))) @@ -514,7 +514,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 ind) + (uninterp_ind_pattern_notations scopes 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 @@ -734,7 +734,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 r'') + extern_notation scopes vars r'' (uninterp_notations scopes r'') with No_match -> lift (fun ?loc -> function | GRef (ref,us) -> extern_global (select_stronger_impargs (implicits_of_global ref)) |