aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/ssreflect/plugin/trunk
diff options
context:
space:
mode:
Diffstat (limited to 'mathcomp/ssreflect/plugin/trunk')
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssreflect.ml43
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssrmatching.ml43
-rw-r--r--mathcomp/ssreflect/plugin/trunk/ssrmatching.mli3
3 files changed, 6 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index e05526e..f3a4f70 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/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/trunk/ssrmatching.ml4 b/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
index aa44fec..39f3e7d 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/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/trunk/ssrmatching.mli b/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
index b7d8d18..74a603e 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssrmatching.mli
+++ b/mathcomp/ssreflect/plugin/trunk/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