diff options
| author | Pierre-Marie Pédrot | 2019-06-09 12:19:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 17:38:35 +0200 |
| commit | e5c788f9efce9a9dd11910cd53c4a99451c48d8a (patch) | |
| tree | 0ef48e2c5e135bc209ffa036454dfe3c760d2046 /test-suite | |
| parent | 3d9f2d1cbc6256c48523db00fa2cc9743a843dfe (diff) | |
Give a functional type to Ltac1 quotations with a context.
This looks more principled, and doesn't require as much tinkering with
the typing implementation.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/compat.v | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/test-suite/ltac2/compat.v b/test-suite/ltac2/compat.v index a24c9af10d..9c11d19c27 100644 --- a/test-suite/ltac2/compat.v +++ b/test-suite/ltac2/compat.v @@ -30,17 +30,14 @@ Fail Ltac2 pose1 (v : constr) := (** Variables explicitly crossing the boundary must satisfy typing properties *) Goal True. Proof. -(* Missing variable *) -Fail ltac1:(x |- idtac). (* Wrong type *) -Fail let x := 0 in ltac1:(x |- idtac). +Fail ltac1:(x |- idtac) 0. (* OK, and runtime has access to variable *) -let x := Ltac1.of_constr constr:(Type) in ltac1:(x |- idtac x). +ltac1:(x |- idtac x) (Ltac1.of_constr constr:(Type)). (* Same for ltac1val *) -Fail Ltac1.run ltac1val:(x |- idtac). -Fail let x := 0 in Ltac1.run ltac1val:(x |- idtac). -let x := Ltac1.of_constr constr:(Type) in Ltac1.run ltac1val:(x |- idtac x). +Fail Ltac1.run (ltac1val:(x |- idtac) 0). +Ltac1.run (ltac1val:(x |- idtac x) (Ltac1.of_constr constr:(Type))). Abort. (** Test calls to Ltac2 from Ltac1 *) |