aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/v8.5
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect/plugin/v8.5')
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssreflect.ml43
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml43
-rw-r--r--mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli3
3 files changed, 6 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
index 20fd720..4bea3b8 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4
@@ -1,4 +1,5 @@
-(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* Distributed under the terms of CeCILL-B. *)
(* This line is read by the Makefile's dist target: do not remove. *)
DECLARE PLUGIN "ssreflect"
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
index 74f42f6..f62e234 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.ml4
@@ -1,4 +1,5 @@
-(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* Distributed under the terms of CeCILL-B. *)
(* Defining grammar rules with "xx" in it automatically declares keywords too,
* we thus save the lexer to restore it at the end of the file *)
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
index b7d8d18..74a603e 100644
--- a/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/v8.5/ssrmatching.mli
@@ -1,4 +1,5 @@
-(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
+(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *)
+(* Distributed under the terms of CeCILL-B. *)
open Genarg
open Tacexpr