diff options
author | Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org> | 2018-06-03 18:26:33 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2018-06-06 17:18:18 +0200 |
commit | b8552c55a3c65a3f598d155aeb764e68841ba501 (patch) | |
tree | bfedb4c0fd97bceb9dd76490913d5049c032be07 /cparser/validator/Tuples.v | |
parent | da76ba512d1efbae8ab5ebcb79eb58c0085a026b (diff) | |
download | compcert-b8552c55a3c65a3f598d155aeb764e68841ba501.tar.gz compcert-b8552c55a3c65a3f598d155aeb764e68841ba501.zip |
Fix menhirLib namespaces, following changes in Menhir version 20180530
Diffstat (limited to 'cparser/validator/Tuples.v')
-rw-r--r-- | cparser/validator/Tuples.v | 49 |
1 files changed, 0 insertions, 49 deletions
diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v deleted file mode 100644 index 3fd2ec03..00000000 --- a/cparser/validator/Tuples.v +++ /dev/null @@ -1,49 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Jacques-Henri Jourdan, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 of the License, or *) -(* (at your option) any later version. This file is also distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -Require Import List. -Require Import Coq.Program.Syntax. -Require Import Equality. - -(** A curryfied function with multiple parameters **) -Definition arrows_left: list Type -> Type -> Type := - fold_left (fun A B => B -> A). - -(** A curryfied function with multiple parameters **) -Definition arrows_right: Type -> list Type -> Type := - fold_right (fun A B => A -> B). - -(** A tuple is a heterogeneous list. For convenience, we use pairs. **) -Fixpoint tuple (types : list Type) : Type := - match types with - | nil => unit - | t::q => prod t (tuple q) - end. - -Fixpoint uncurry {args:list Type} {res:Type}: - arrows_left args res -> tuple args -> res := - match args return forall res, arrows_left args res -> tuple args -> res with - | [] => fun _ f _ => f - | t::q => fun res f p => let (d, t) := p in - (@uncurry q _ f t) d - end res. - -Lemma JMeq_eqrect: - forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b), - eq_rect a P x b e ~= x. -Proof. -destruct e. -reflexivity. -Qed. |