Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 9 insertions, 10 deletions

diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 9eaa91cc..ae82153d 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -1,18 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: redexpr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Term
 open Closure
 open Pattern
-open Rawterm
+open Glob_term
 open Reductionops
 open Termops
 
@@ -22,23 +20,24 @@ type red_expr =
 val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
-(* [true] if we should use the vm to verify the reduction *)
 
-(* Adding a custom reduction (function to be use at the ML level)
+(** [true] if we should use the vm to verify the reduction *)
+
+(** Adding a custom reduction (function to be use at the ML level)
    NB: the effect is permanent. *)
 val declare_reduction : string -> reduction_function -> unit
 
-(* Adding a custom reduction (function to be called a vernac command).
+(** Adding a custom reduction (function to be called a vernac command).
    The boolean flag is the locality. *)
 val declare_red_expr : bool -> string -> red_expr -> unit
 
-(* Opaque and Transparent commands. *)
+(** Opaque and Transparent commands. *)
 
-(* Sets the expansion strategy of a constant. When the boolean is
+(** Sets the expansion strategy of a constant. When the boolean is
    true, the effect is non-synchronous (i.e. it does not survive
    section and module closure). *)
 val set_strategy :
   bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
 
-(* call by value normalisation function using the virtual machine *)
+(** call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function