diff options
| -rw-r--r-- | interp/constrextern.ml | 7 | ||||
| -rw-r--r-- | tactics/extraargs.ml4 | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations2.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations2.v | 9 |
4 files changed, 20 insertions, 4 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 24f5a78c5..99c627a95 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -592,6 +592,10 @@ let rec remove_coercions inctx = function with Not_found -> c) | c -> c +let rec flatten_application = function + | RApp (loc,RApp(_,a,l'),l) -> flatten_application (RApp (loc,a,l'@l)) + | a -> a + let rec rename_rawconstr_var id0 id1 = function RRef(loc,VarRef id) when id=id0 -> RRef(loc,VarRef id1) | RVar(loc,id) when id=id0 -> RVar(loc,id1) @@ -632,8 +636,9 @@ let rec extern inctx scopes vars r = extern_optimal_prim_token scopes r r' with No_match -> try + let r'' = flatten_application r' in if !Flags.raw_print or !print_no_symbol then raise No_match; - extern_symbol scopes vars r' (uninterp_notations r') + extern_symbol scopes vars r'' (uninterp_notations r'') with No_match -> match r' with | RRef (loc,ref) -> extern_global loc (implicits_of_global ref) diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index e6eefea8a..adf8275ee 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -184,7 +184,7 @@ ARGUMENT EXTEND hloc let pr_by_arg_tac _prc _prlc prtac opt_c = match opt_c with | None -> mt () - | Some t -> spc () ++ hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Ppextend.E) t) ARGUMENT EXTEND by_arg_tac TYPED AS tactic_opt @@ -200,8 +200,8 @@ let pr_in_hyp pr_id (lo,concl) : Pp.std_ppcmds = | None,true -> str "in" ++ spc () ++ str "*" | None,false -> str "in" ++ spc () ++ str "*" ++ spc () ++ str "|-" | Some l,_ -> - str "in" ++ spc () ++ - Util.prlist_with_sep spc pr_id l ++ + str "in" ++ + Util.prlist (fun id -> spc () ++ pr_id id) l ++ match concl with | true -> spc () ++ str "|-" ++ spc () ++ str "*" | _ -> mt () diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index aca872970..c1a7e961a 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -1,4 +1,6 @@ 2 3 : PAIR +2[+]3 + : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 0d5cc9e24..3eeff401c 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -6,6 +6,15 @@ Inductive PAIR := P (n1:nat) (n2:nat). Coercion P : nat >-> Funclass. Check (2 3). +(* Check that notations with coercions to functions inserted still work *) +(* (were not working from revision 11886 to 12951) *) + +Record Binop := { binop :> nat -> nat -> nat }. +Class Plusop := { plusop : Binop; z : nat }. +Infix "[+]" := plusop (at level 40). +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}. +Check 2[+]3. + (* Test bug #2091 (variable le was printed using <= !) *) Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. |