diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-10-21 10:49:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-10-21 12:24:43 +0200 |
| commit | 5b0b6c92354c34a4f0d5551f88b16264fb08be5f (patch) | |
| tree | b789f64d3024e70a70a1c175facab638dde76367 /test-suite/output/unifconstraints.out | |
| parent | a5b977e3acb6d2cd73ed6c895a7d4b587366caa9 (diff) | |
This makes [refine] typecheck the term only once (instead of twice),
(Qed excluded of course). Fix test-suite file for output of constraints
accordingly.
Diffstat (limited to 'test-suite/output/unifconstraints.out')
| -rw-r--r-- | test-suite/output/unifconstraints.out | 26 |
1 files changed, 4 insertions, 22 deletions
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out index d152052ba..ae8460362 100644 --- a/test-suite/output/unifconstraints.out +++ b/test-suite/output/unifconstraints.out @@ -8,11 +8,7 @@ subgoal 2 is: forall n : nat, ?Goal n -> ?Goal (S n) subgoal 3 is: nat -unification constraints: - ?Goal ?Goal2 <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal ?Goal2 <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -28,11 +24,7 @@ subgoal 2 is: forall n0 : nat, ?Goal@{n:=n; m:=m} n0 -> ?Goal@{n:=n; m:=m} (S n0) subgoal 3 is: nat -unification constraints: - ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: ?Goal@{n:=n; m:=m} ?Goal2@{n:=n; m:=m} <= True /\ True /\ True \/ veeryyyyyyyyyyyyloooooooooooooonggidentifier = @@ -48,12 +40,7 @@ subgoal 2 is: forall n0 : nat, ?Goal1@{m:=m} n0 -> ?Goal1@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal1@{m:=m} ?Goal0@{n:=n; m:=m} <= True /\ True /\ True \/ @@ -70,12 +57,7 @@ subgoal 2 is: forall n0 : nat, ?Goal0@{m:=m} n0 -> ?Goal0@{m:=m} (S n0) subgoal 3 is: nat -unification constraints: - - n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= - True /\ True /\ True \/ - veeryyyyyyyyyyyyloooooooooooooonggidentifier = - veeryyyyyyyyyyyyloooooooooooooonggidentifier +unification constraint: n, m : nat |- ?Goal0@{m:=m} ?Goal2@{n:=n} <= True /\ True /\ True \/ |