Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

24 files changed, 60 insertions, 62 deletions

diff --git a/plugins/micromega/Env.v b/plugins/micromega/Env.v
index dd4d596f21..a19e9df904 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.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/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index 62a7333d55..fd4bb248bf 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.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/micromega/Lia.v b/plugins/micromega/Lia.v
index 7242558552..3e58e81ac2 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.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/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 8b959c2784..0a41af4543 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.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/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 34b8bbdd33..72b4dcb6e3 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.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/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 31d051cb4d..ba1f8956e3 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.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        *)
@@ -69,7 +69,7 @@ Ltac xpsatz dom d :=
   end in tac.
 
 Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
-Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 6c157def8f..432683635f 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.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/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index e9ab696264..72353a99e5 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.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/micromega/Refl.v b/plugins/micromega/Refl.v
index 499a8c4c48..32ddb3cf4c 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index a0545637dd..751a81df12 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.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/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 39d0c6b197..391231afd9 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.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/micromega/VarMap.v b/plugins/micromega/VarMap.v
index 6e1fe2220e..4981ddb302 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  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/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 4c4b81a07f..bd425e6bbf 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.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/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index 84a8d13c2d..d7ddef2be4 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.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/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 63485ab269..914881db0d 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.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/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ef1169342f..27daa7e3c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.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        *)
@@ -20,6 +20,7 @@ open Pp
 open Mutils
 open Proofview
 open Goptions
+open Proofview.Notations
 
 (**
   * Debug flag 
@@ -81,10 +82,10 @@ let _ =
    optread = (fun () -> !lia_enum);
    optwrite = (fun x -> lia_enum := x)
   } in
- ignore (declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth)) ;
- ignore (declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth)) ;
- ignore (declare_bool_option lia_enum_opt)
-
+ let _ = declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth) in
+ let _ = declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth) in 
+ let _ = declare_bool_option lia_enum_opt in
+ ()
  
 (**
   * Initialize a tag type to the Tag module declaration (see Mutils).
@@ -887,7 +888,7 @@ struct
 
 
   let is_convertible gl t1 t2 = 
-   Reductionops.is_conv (Tacmach.New.pf_env gl) (Goal.sigma gl) t1 t2
+   Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
 
   let parse_zop gl (op,args) =
    match kind_of_term op with
@@ -1168,8 +1169,8 @@ struct
       with e when Errors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-     let ty   = Typing.unsafe_type_of (Goal.env gl) (Goal.sigma gl) term in
-     let sort = Typing.sort_of (Goal.env gl) (ref (Goal.sigma gl)) ty in
+     let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
+     let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
      Term.is_prop_sort sort in
      
     let rec xparse_formula env tg term =
@@ -1444,8 +1445,8 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) env in
  (* todo : directly generate the proof term - or generalize before conversion? *)
-  Proofview.Goal.nf_enter
-  begin fun gl -> 
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+   let gl = Tacmach.New.of_old (fun x -> x) gl in
    Tacticals.New.tclTHENLIST
     [
      Tactics.change_concl
@@ -1457,12 +1458,12 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
 	[["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
        ("__wit", cert, cert_typ)
       ]
-      (Tacmach.New.pf_concl gl))
+      (Tacmach.pf_concl gl))
    ;
    Tactics.new_generalize env ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
-  end
+  end }
 
 
 (**
@@ -1707,11 +1708,10 @@ let micromega_gen
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
     spec prover =
- Proofview.Goal.nf_enter
-  begin 
-   fun gl -> 
-    let concl = Tacmach.New.pf_concl gl in
-    let hyps  = Tacmach.New.pf_hyps_types gl in
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
+    let concl = Tacmach.pf_concl gl in
+    let hyps  = Tacmach.pf_hyps_types gl in
     try
      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
      let env = Env.elements env in
@@ -1735,7 +1735,7 @@ let micromega_gen
                             ^ "the use of a specialized external tool called csdp. \n\n" 
                             ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
                             ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-  end
+  end }
 
 let micromega_gen parse_arith 
     (negate:'cst atom -> 'cst mc_cnf)
@@ -1756,9 +1756,8 @@ let micromega_order_changer cert env ff  =
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
- Proofview.Goal.nf_enter
-  begin 
-   fun gl -> 
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
     Tacticals.New.tclTHENLIST
      [
      (Tactics.change_concl
@@ -1770,11 +1769,11 @@ let micromega_order_changer cert env ff  =
 	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
          ("__wit", cert, cert_typ)
         ]
-        (Tacmach.New.pf_concl gl)));
+        (Tacmach.pf_concl gl)));
       Tactics.new_generalize env ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
-  end
+  end }
 
 
 let micromega_genr prover =
@@ -1790,11 +1789,10 @@ let micromega_genr prover =
     proof_typ = Lazy.force coq_QWitness ;
     dump_proof = dump_psatz coq_Q dump_q
   } in
-  Proofview.Goal.nf_enter
-   begin 
-    fun gl -> 
-     let concl = Tacmach.New.pf_concl gl in
-     let hyps  = Tacmach.New.pf_hyps_types gl in
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+     let gl = Tacmach.New.of_old (fun x -> x) gl in
+     let concl = Tacmach.pf_concl gl in
+     let hyps  = Tacmach.pf_hyps_types gl in
      try
       let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
        let env = Env.elements env in
@@ -1822,7 +1820,7 @@ let micromega_genr prover =
       ^ "the use of a specialized external tool called csdp. \n\n" 
       ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
        ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
-    end
+    end }
 
 
 let micromega_genr prover  = (micromega_genr prover)
diff --git a/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index b41f29c981..2536005ede 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.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/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 62f0ae5037..bca1c2febd 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.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        *)
@@ -18,15 +18,15 @@
 
 open Errors
 open Misctypes
+open Stdarg
+open Constrarg
+open Pcoq.Prim
+open Pcoq.Tactic
 
 DECLARE PLUGIN "micromega_plugin"
 
-let out_arg = function
-  | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
-  | ArgArg x -> x
-
 TACTIC EXTEND PsatzZ
-| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z (out_arg i)) ]
+| [ "psatz_Z" int_or_var(i) ] -> [  (Coq_micromega.psatz_Z i) ]
 | [ "psatz_Z" ] -> [  (Coq_micromega.psatz_Z (-1)) ]
 END
 
@@ -63,12 +63,12 @@ TACTIC EXTEND LRA_R
 END
 
 TACTIC EXTEND PsatzR
-| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R (out_arg i)) ]
+| [ "psatz_R" int_or_var(i) ] -> [   (Coq_micromega.psatz_R i) ]
 | [ "psatz_R" ] -> [   (Coq_micromega.psatz_R (-1)) ]
 END
 
 TACTIC EXTEND PsatzQ
-| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q (out_arg i)) ]
+| [ "psatz_Q" int_or_var(i) ] -> [  (Coq_micromega.psatz_Q i) ]
 | [ "psatz_Q" ] -> [  (Coq_micromega.psatz_Q (-1)) ]
 END
 
diff --git a/plugins/micromega/mfourier.ml b/plugins/micromega/mfourier.ml
index 0247204490..e22fe58434 100644
--- a/plugins/micromega/mfourier.ml
+++ b/plugins/micromega/mfourier.ml
@@ -23,7 +23,7 @@ struct
 	  - None , Some v -> \]-oo,v\]
 	  - Some v, None  -> \[v,+oo\[
 	  - Some v, Some v' -> \[v,v'\]
-      Intervals needs to be explicitely normalised.
+      Intervals needs to be explicitly normalised.
       *)
 
   type who = Left | Right
@@ -120,7 +120,7 @@ and cstr_info = {
 (** A system of constraints has the form [\{sys = s ; vars = v\}].
     [s] is a hashtable mapping a normalised vector to a [cstr_info] record where
     - [bound] is an interval
-    - [prf_idx] is the set of hypothese indexes (i.e. constraints in the initial system) used to obtain the current constraint.
+    - [prf_idx] is the set of hypothesis indexes (i.e. constraints in the initial system) used to obtain the current constraint.
        In the initial system, each constraint is given an unique singleton proof_idx.
        When a new constraint c is computed by a function f(c1,...,cn), its proof_idx is ISet.fold union (List.map (fun x -> x.proof_idx) [c1;...;cn]
     - [pos] is the number of positive values of the vector
@@ -872,7 +872,7 @@ let  mk_proof hyps prf =
       | Elim(v,prf1,prf2) ->
           let prfsl = mk_proof prf1
           and prfsr = mk_proof prf2 in
-            (* I take only the pairs for which the elimination is meaningfull *)
+            (* I take only the pairs for which the elimination is meaningful *)
             forall_pairs (pivot v) prfsl prfsr
       | And(prf1,prf2) ->
           let prfsl1 = mk_proof prf1
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 465c7afcee..c13e8fc28f 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.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/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 2dc0d00323..6a03e2d61f 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.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/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index b8b42a3f25..90a108a3b7 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.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/micromega/sos.mli b/plugins/micromega/sos.mli
index fc0b2fd466..1ca27ea20a 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.mli
@@ -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/micromega/sos_types.ml b/plugins/micromega/sos_types.ml
index e95437141c..615ac5a2fb 100644
--- a/plugins/micromega/sos_types.ml
+++ b/plugins/micromega/sos_types.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        *)