diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/Fourier.v | 2 | ||||
| -rw-r--r-- | plugins/fourier/Fourier_util.v | 2 | ||||
| -rw-r--r-- | plugins/fourier/fourier.ml | 2 | ||||
| -rw-r--r-- | plugins/fourier/fourierR.ml | 9 | ||||
| -rw-r--r-- | plugins/fourier/g_fourier.ml4 | 2 |
5 files changed, 10 insertions, 7 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v index 1832de85b3..1d7ee93ea3 100644 --- a/plugins/fourier/Fourier.v +++ b/plugins/fourier/Fourier.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v index 284d220afe..d4b0e2e107 100644 --- a/plugins/fourier/Fourier_util.v +++ b/plugins/fourier/Fourier_util.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml index 50a5150ddc..4919232c98 100644 --- a/plugins/fourier/fourier.ml +++ b/plugins/fourier/fourier.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index b1f642c1d2..dc5dd45ab0 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -16,7 +16,6 @@ open Term open Tactics open Names open Globnames -open Tacmach open Fourier open Contradiction open Proofview.Notations @@ -445,7 +444,11 @@ let is_ineq (h,t) = ;; *) -let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;; +let list_of_sign s = + let open Context.Named.Declaration in + List.map (function LocalAssum (name, typ) -> name, typ + | LocalDef (name, _, typ) -> name, typ) + s;; let mkAppL a = let l = Array.to_list a in diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4 index d00f0564f7..7c665ae7b5 100644 --- a/plugins/fourier/g_fourier.ml4 +++ b/plugins/fourier/g_fourier.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |