Made pretyping a functor over a coercion implementation. Pretyping.Default uses the original Coercion implementation.

Updated contributions that called pretyping to use the default impl.
Also update subtac using the functor, do some renamings and add interfaces for all files.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8654 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 28 insertions, 24 deletions

diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index f5356d432c..cc2211f5f8 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -19,28 +19,32 @@ open Evarutil
 open Rawterm
 (*i*)
 
-(*s Coercions. *)
+module type S = sig
+  (*s Coercions. *)
+  
+  (* [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type a product; it returns [j] if no coercion is applicable *)
+  val inh_app_fun :
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
+    
+  (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
+     inserts a coercion into [j], if needed, in such a way it gets as
+     type a sort; it fails if no coercion is applicable *)
+  val inh_coerce_to_sort : loc ->
+    env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
+    
+  (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
+     [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
+     [j.uj_type] are convertible; it fails if no coercion is applicable *)
+  val inh_conv_coerce_to : loc -> 
+    env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
+    
+  (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
+     pattern [pat] typed in [ind1] into a pattern typed in [ind2];
+     raises [Not_found] if no coercion found *)
+  val inh_pattern_coerce_to :
+    loc  -> cases_pattern -> inductive -> inductive -> cases_pattern
+end
 
-(* [inh_app_fun env isevars j] coerces [j] to a function; i.e. it
-   inserts a coercion into [j], if needed, in such a way it gets as
-   type a product; it returns [j] if no coercion is applicable *)
-val inh_app_fun :
-  env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment
-
-(* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it
-   inserts a coercion into [j], if needed, in such a way it gets as
-   type a sort; it fails if no coercion is applicable *)
-val inh_coerce_to_sort : loc ->
-  env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment
-
-(* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type 
-   [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and
-   [j.uj_type] are convertible; it fails if no coercion is applicable *)
-val inh_conv_coerce_to : loc -> 
-  env -> evar_defs -> unsafe_judgment -> types -> evar_defs * unsafe_judgment
-
-(* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases
-   pattern [pat] typed in [ind1] into a pattern typed in [ind2];
-   raises [Not_found] if no coercion found *)
-val inh_pattern_coerce_to :
-  loc  -> cases_pattern -> inductive -> inductive -> cases_pattern
+module Default : S