From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 kernel/retroknowledge.mli | 40 ++++++++++++++++++++--------------------
 1 file changed, 20 insertions(+), 20 deletions(-)

(limited to 'kernel/retroknowledge.mli')

diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index ee3fccd5..0f1cdc8e 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: retroknowledge.mli 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -24,8 +24,8 @@ type nat_field =
   | NatType
   | NatPlus
   | NatTimes
-  
-type n_field = 
+
+type n_field =
   | NPositive
   | NType
   | NTwice
@@ -35,7 +35,7 @@ type n_field =
   | NPlus
   | NTimes
 
-type int31_field = 
+type int31_field =
   | Int31Bits
   | Int31Type
   | Int31Twice
@@ -81,14 +81,14 @@ val initial_retroknowledge : retroknowledge
    returns the compilation of id in cont if it has a specific treatment
    or raises Not_found if id should be compiled as usual *)
 val get_vm_compiling_info  : retroknowledge -> entry -> Cbytecodes.comp_env ->
-                             constr array -> 
+                             constr array ->
                              int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes
 (*Given an identifier id (usually Construct _)
    and its argument array, returns a function that tries an ad-hoc optimisated
    compilation (in the case of the 31-bit integers it means compiling them
    directly into an integer)
    raises Not_found if id should be compiled as usual, and expectingly
-   CBytecodes.NotClosed if the term is not a closed constructor pattern 
+   CBytecodes.NotClosed if the term is not a closed constructor pattern
    (a constant for the compiler) *)
 val get_vm_constant_static_info : retroknowledge -> entry ->
                                    constr array ->
@@ -99,19 +99,19 @@ val get_vm_constant_static_info : retroknowledge -> entry ->
    of id+args+cont when id has a specific treatment (in the case of
    31-bit integers, that would be the dynamic compilation into integers)
    or raises Not_found if id should be compiled as usual *)
-val get_vm_constant_dynamic_info : retroknowledge -> entry -> 
-                                Cbytecodes.comp_env -> 
-                                Cbytecodes.block array -> 
+val get_vm_constant_dynamic_info : retroknowledge -> entry ->
+                                Cbytecodes.comp_env ->
+                                Cbytecodes.block array ->
                                 int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes
-(* Given a type identifier, this function is used before compiling a match 
-   over this type. In the case of 31-bit integers for instance, it is used 
+(* Given a type identifier, this function is used before compiling a match
+   over this type. In the case of 31-bit integers for instance, it is used
    to add the instruction sequence which would perform a dynamic decompilation
    in case the argument of the match is not in coq representation *)
 val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes
                                                        -> Cbytecodes.bytecodes
 
-(* Given a type identifier, this function is used by pretyping/vnorm.ml to 
-   recover the elements of that type from their compiled form if it's non 
+(* Given a type identifier, this function is used by pretyping/vnorm.ml to
+   recover the elements of that type from their compiled form if it's non
    standard (it is used (and can be used) only when the compiled form
    is not a block *)
 val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr
@@ -127,26 +127,26 @@ val find : retroknowledge -> field -> entry
 (* the following function manipulate the reactive information of values
    they are only used by the functions of Pre_env, and Environ to implement
    the functions register and unregister of Environ *)
-val add_vm_compiling_info : retroknowledge-> entry -> 
+val add_vm_compiling_info : retroknowledge-> entry ->
                             (bool -> Cbytecodes.comp_env -> constr array -> int ->
                             Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
                             retroknowledge
-val add_vm_constant_static_info : retroknowledge-> entry -> 
+val add_vm_constant_static_info : retroknowledge-> entry ->
                                   (bool->constr array->
                                       Cbytecodes.structured_constant) ->
                                   retroknowledge
-val add_vm_constant_dynamic_info : retroknowledge-> entry -> 
-                                   (bool -> Cbytecodes.comp_env -> 
-                                   Cbytecodes.block array -> int -> 
+val add_vm_constant_dynamic_info : retroknowledge-> entry ->
+                                   (bool -> Cbytecodes.comp_env ->
+                                   Cbytecodes.block array -> int ->
                                    Cbytecodes.bytecodes -> Cbytecodes.bytecodes) ->
                                    retroknowledge
 val add_vm_before_match_info : retroknowledge -> entry ->
                               (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) ->
                               retroknowledge
 
-val add_vm_decompile_constant_info : retroknowledge -> entry -> 
+val add_vm_decompile_constant_info : retroknowledge -> entry ->
                                     (int -> constr) -> retroknowledge
-                                      
+
 
 val clear_info : retroknowledge-> entry -> retroknowledge
 
-- 
cgit v1.2.3