diff options
| -rw-r--r-- | interp/constrextern.ml | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations5.out | 20 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 24 |
3 files changed, 28 insertions, 22 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 38dc10a9b3..82ba559406 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -742,7 +742,7 @@ let extern_applied_ref inctx impl (cf,f) us args = let extern_applied_syntactic_definition n extraimpl (cf,f) syndefargs extraargs = try let syndefargs = List.map (fun a -> (a,None)) syndefargs in - let extraargs = adjust_implicit_arguments false (List.length extraargs) 1 extraargs extraimpl in + let extraargs = adjust_implicit_arguments false n (n-List.length extraargs+1) extraargs extraimpl in let args = syndefargs @ extraargs in if args = [] then cf else CApp ((None, CAst.make cf), args) with Expl -> @@ -762,8 +762,10 @@ let extern_applied_notation n impl f args = if List.is_empty args then f.CAst.v else - let args = adjust_implicit_arguments false (List.length args) 1 args impl in + try + let args = adjust_implicit_arguments false n (n-List.length args+1) args impl in mkFlattenedCApp (f,args) + with Expl -> raise No_match let extern_args extern env args = let map (arg, argscopes) = lazy (extern argscopes env arg) in diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index c5b4d6f291..96687ed07f 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -138,7 +138,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -158,7 +158,7 @@ v 0 : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -v 0 (B:=bool) true +v 0 true : 0 = 0 /\ true = true v : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b @@ -188,9 +188,9 @@ where : forall b : ?B, 0 = 0 /\ b = b where ?B : [ |- Type] -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b @@ -226,23 +226,27 @@ p 0 0 true : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b ## 0 : forall (a2 : nat) (B : Type) (b : B), 0 = a2 /\ b = b +@p nat 0 0 + : forall (B : Type) (b : B), 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b ## 0 0 (B:=bool) : forall b : bool, 0 = 0 /\ b = b -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true -## 0 0 (B:=bool) true +## 0 0 true : 0 = 0 /\ true = true diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index b3bea929ba..3c25547aac 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -181,7 +181,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -209,7 +209,7 @@ Module AppliedTermsPrinting. Check v 0. (* v 0 *) Check v 0 true. - (* v 0 (B:=bool) true -- BUG *) + (* v 0 true *) Check @p nat 0. (* v *) Check @p nat 0 0. @@ -243,9 +243,9 @@ Module AppliedTermsPrinting. Check ## 0 0. (* ## 0 0 *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 (B:=bool). @@ -298,16 +298,16 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* @p nat 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 bool. (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENT parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true -- INCONSISTENT parsing/printing *) End NotationForPartialApplication. @@ -324,16 +324,16 @@ Module AppliedTermsPrinting. (* ## 0 *) Check ## 0. (* ## 0 *) - (* Check ## 0 0. *) - (* Anomaly *) + Check ## 0 0. + (* @p nat 0 0 *) Check p 0 0 (B:=bool). (* ## 0 0 (B:=bool) *) Check ## 0 0 bool. (* ## 0 0 (B:=bool) -- INCONSISTENT parsing/printing *) Check p 0 0 true. - (* ## 0 0 (B:=bool) true -- BUG B should not be displayed *) + (* ## 0 0 true *) Check ## 0 0 bool true. - (* ## 0 0 (B:=bool) true -- INCONSISTENCY parsing/printing + BUG B should not be displayed *) + (* ## 0 0 true -- INCONSISTENCY parsing/printing *) End AtNotationForPartialApplication. |