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

7 files changed, 957 insertions, 799 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index f5dd223283..b2ef8060d6 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,6 +63,19 @@ let error_wrong_predicate_arity_loc loc env c n1 n2 =
 let error_needs_inversion env x t =
   raise (PatternMatchingError (env, NeedsInversion (x,t)))
 
+module type S = sig
+  val compile_cases :
+    loc ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
+      Evd.evar_defs ref ->
+    type_constraint -> 
+    env ->
+    rawconstr option *
+      (rawconstr * (name * (loc * inductive * name list) option)) list *
+      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    unsafe_judgment
+end
+
 (************************************************************************)
 (*            Pattern-matching compilation (Cases)                      *)
 (************************************************************************)
@@ -371,6 +384,9 @@ let evd_comb2 f isevars x y =
   isevars := evd';
   y
 
+
+module Cases_F(Coercion : Coercion.S) : S = struct
+
 let adjust_tomatch_to_pattern pb ((current,typ),deps) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
@@ -1654,46 +1670,47 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
 
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
-
-let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
-
-  (* We build the matrix of patterns and right-hand-side *)
-  let matx = matx_of_eqns env tomatchl eqns in
-
-  (* We build the vector of terms to match consistently with the *)
-  (* constructors found in patterns *)
-  let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
-
-  (* We build the elimination predicate if any and check its consistency *)
-  (* with the type of arguments to match *)
-  let tmsign = List.map snd tomatchl in
-  let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
-
-  (* We deal with initial aliases *)
-  let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
-
-  (* We push the initial terms to match and push their alias to rhs' envs *)
-  (* names of aliases will be recovered from patterns (hence Anonymous here) *)
-  let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
- 
-  let pb =
-    { env      = env;
-      isevars  = isevars;
-      pred     = pred;
-      tomatch  = initial_pushed;
-      history  = start_history (List.length initial_pushed);
-      mat      = matx;
-      caseloc  = loc;
-      typing_function = typing_fun } in
-  
-  let _, j = compile pb in
-
-  (* We check for unused patterns *)
-  List.iter (check_unused_pattern env) matx;
   
-  match tycon with
-    | Some p ->
-	let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
-        isevars := evd';
-        j
-    | None -> j
+  let compile_cases loc (typing_fun, isevars) tycon env (predopt, tomatchl, eqns)=
+    
+    (* We build the matrix of patterns and right-hand-side *)
+    let matx = matx_of_eqns env tomatchl eqns in
+      
+    (* We build the vector of terms to match consistently with the *)
+    (* constructors found in patterns *)
+    let tomatchs = coerce_to_indtype typing_fun isevars env matx tomatchl in
+      
+    (* We build the elimination predicate if any and check its consistency *)
+    (* with the type of arguments to match *)
+    let tmsign = List.map snd tomatchl in
+    let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
+      
+    (* We deal with initial aliases *)
+    let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
+      
+    (* We push the initial terms to match and push their alias to rhs' envs *)
+    (* names of aliases will be recovered from patterns (hence Anonymous here) *)
+    let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in
+      
+    let pb =
+      { env      = env;
+	isevars  = isevars;
+	pred     = pred;
+	tomatch  = initial_pushed;
+	history  = start_history (List.length initial_pushed);
+	mat      = matx;
+	caseloc  = loc;
+	typing_function = typing_fun } in
+      
+    let _, j = compile pb in
+      
+      (* We check for unused patterns *)
+      List.iter (check_unused_pattern env) matx;
+      
+      match tycon with
+	| Some p ->
+	    let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in
+              isevars := evd';
+              j
+	| None -> j
+end
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index f08b2c4a3c..e9fba44d22 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -38,13 +38,17 @@ val error_wrong_numarg_inductive_loc : loc -> env -> inductive -> int -> 'a
 
 (*s Compilation of pattern-matching. *)
 
-val compile_cases :
-  loc ->
-  (type_constraint -> env -> rawconstr -> unsafe_judgment) *
-  evar_defs ref ->
-  type_constraint -> 
-  env ->
-  rawconstr option *
-  (rawconstr * (name * (loc * inductive * name list) option)) list *
-  (loc * identifier list * cases_pattern list * rawconstr) list ->
-  unsafe_judgment
+module type S = sig
+  val compile_cases :
+    loc ->
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
+      evar_defs ref ->
+    type_constraint -> 
+    env ->
+    rawconstr option *
+      (rawconstr * (name * (loc * inductive * name list) option)) list *
+      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    unsafe_judgment
+end
+
+module Cases_F(C : Coercion.S) : S
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 6c4dbf5ed8..cb8c2cf2b5 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -31,7 +31,7 @@ open Mod_subst
 (* *)
 let w_coerce env c ctyp target evd =
   let j = make_judge c ctyp in
-  let (evd',j') = Coercion.inh_conv_coerce_to dummy_loc env evd j target in
+  let (evd',j') = Coercion.Default.inh_conv_coerce_to dummy_loc env evd j target in
   (evd',j'.uj_val)
 
 let pf_env gls = Global.env_of_context gls.it.evar_hyps
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index d2c3e255c5..3b2d85b1ff 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -21,159 +21,188 @@ open Evarconv
 open Retyping
 open Evd
 
-(* Typing operations dealing with coercions *)
-
-let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
-
-(* Here, funj is a coercion therefore already typed in global context *)
-let apply_coercion_args env argl funj =
-  let rec apply_rec acc typ = function
-    | [] -> { uj_val = applist (j_val funj,argl);
-              uj_type = typ }
-    | h::restl ->
-    (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
-  	match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
-	  | Prod (_,c1,c2) -> 
-              (* Typage garanti par l'appel à app_coercion*)
-	      apply_rec (h::acc) (subst1 h c2) restl
-	  | _ -> anomaly "apply_coercion_args"
-  in 
-  apply_rec [] funj.uj_type argl
-
-exception NoCoercion
-
-(* appliquer le chemin de coercions de patterns p *)
-
-let apply_pattern_coercion loc pat p =
-  List.fold_left
-    (fun pat (co,n) ->
-       let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
-       Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
-    pat p
-
-(* raise Not_found if no coercion found *)
-let inh_pattern_coerce_to loc pat ind1 ind2 =
-  let i1 = inductive_class_of ind1 in
-  let i2 = inductive_class_of ind2 in
-  let p = lookup_pattern_path_between (i1,i2) in
-  apply_pattern_coercion loc pat p
-
-(* appliquer le chemin de coercions p à hj *)
-
-let apply_coercion env p hj typ_cl =
-  try 
-    fst (List.fold_left
-           (fun (ja,typ_cl) i -> 
-              let fv,isid = coercion_value i in
-              let argl = (class_args_of typ_cl)@[ja.uj_val] in
-              let jres = apply_coercion_args env argl fv in
-              (if isid then 
-		 { uj_val = ja.uj_val; uj_type = jres.uj_type }
-               else 
-		 jres),
-	      jres.uj_type)
-           (hj,typ_cl) p)
-  with _ -> anomaly "apply_coercion"
-
-let inh_app_fun env isevars j = 
-  let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
-  match kind_of_term t with
-    | Prod (_,_,_) -> (isevars,j)
-    | Evar ev when not (is_defined_evar isevars ev) ->
-	let (isevars',t) = define_evar_as_arrow isevars ev in
-	(isevars',{ uj_val = j.uj_val; uj_type = t })
-    | _ ->
-       	(try
- 	   let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-      	   let p = lookup_path_to_fun_from i1 in
-           (isevars,apply_coercion env p j t)
-	 with Not_found -> (isevars,j))
-
-let inh_tosort_force loc env isevars j =
-  try
-    let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
-    let p = lookup_path_to_sort_from i1 in
-    let j1 = apply_coercion env p j t in 
-    (isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
-  with Not_found ->
-    error_not_a_type_loc loc env (evars_of isevars) j
-
-let inh_coerce_to_sort loc env isevars j =
-  let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
-  match kind_of_term typ with
-    | Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
-    | Evar ev when not (is_defined_evar isevars ev) ->
-	let (isevars',s) = define_evar_as_sort isevars ev in
-	(isevars',{ utj_val = j.uj_val; utj_type = s })
-    | _ ->
-	inh_tosort_force loc env isevars j
-
-let inh_coerce_to_fail env isevars c1 hj =
-  let hj' =
+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  -> Rawterm.cases_pattern -> inductive -> inductive -> Rawterm.cases_pattern
+end
+
+module Default = struct
+  (* Typing operations dealing with coercions *)
+  exception NoCoercion
+
+  let class_of1 env sigma t = class_of env sigma (nf_evar sigma t)
+
+  (* Here, funj is a coercion therefore already typed in global context *)
+  let apply_coercion_args env argl funj =
+    let rec apply_rec acc typ = function
+      | [] -> { uj_val = applist (j_val funj,argl);
+		uj_type = typ }
+      | h::restl ->
+	  (* On devrait pouvoir s'arranger pour qu'on n'ait pas à faire hnf_constr *)
+  	  match kind_of_term (whd_betadeltaiota env Evd.empty typ) with
+	    | Prod (_,c1,c2) -> 
+		(* Typage garanti par l'appel à app_coercion*)
+		apply_rec (h::acc) (subst1 h c2) restl
+	    | _ -> anomaly "apply_coercion_args"
+    in 
+      apply_rec [] funj.uj_type argl
+
+  (* appliquer le chemin de coercions de patterns p *)
+
+  let apply_pattern_coercion loc pat p =
+    List.fold_left
+      (fun pat (co,n) ->
+	 let f i = if i<n then Rawterm.PatVar (loc, Anonymous) else pat in
+	   Rawterm.PatCstr (loc, co, list_tabulate f (n+1), Anonymous))
+      pat p
+
+  (* raise Not_found if no coercion found *)
+  let inh_pattern_coerce_to loc pat ind1 ind2 =
+    let i1 = inductive_class_of ind1 in
+    let i2 = inductive_class_of ind2 in
+    let p = lookup_pattern_path_between (i1,i2) in
+      apply_pattern_coercion loc pat p
+
+  (* appliquer le chemin de coercions p à hj *)
+
+  let apply_coercion env p hj typ_cl =
     try 
-      let t1,i1 = class_of1 env (evars_of isevars) c1 in
-      let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
-      let p = lookup_path_between (i2,i1) in
-      apply_coercion env p hj t2
-    with Not_found -> raise NoCoercion 
-  in
-  try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
-  with Reduction.NotConvertible -> raise NoCoercion
-
-let rec inh_conv_coerce_to_fail env isevars hj c1 =
-  let {uj_val = v; uj_type = t} = hj in
-  try (the_conv_x_leq env t c1 isevars, hj)
-  with Reduction.NotConvertible ->
-    (try 
-      inh_coerce_to_fail env isevars c1 hj
-    with NoCoercion ->
-      (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
-	     kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
-	 | Prod (_,t1,t2), Prod (name,u1,u2) -> 
-             let v' = whd_betadeltaiota env (evars_of isevars) v in
-             let (evd',b) =
-               match kind_of_term v' with
-                 | Lambda (_,v1,v2) ->
-                     (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
-                     with Reduction.NotConvertible -> (isevars, false))
-                 | _  -> (isevars,false) in
-             if b
-             then 
-	       let (x,v1,v2) = destLambda v' in
-               let env1 = push_rel (x,None,v1) env in
-               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
+      fst (List.fold_left
+             (fun (ja,typ_cl) i -> 
+		let fv,isid = coercion_value i in
+		let argl = (class_args_of typ_cl)@[ja.uj_val] in
+		let jres = apply_coercion_args env argl fv in
+		  (if isid then 
+		     { uj_val = ja.uj_val; uj_type = jres.uj_type }
+		   else 
+		     jres),
+		jres.uj_type)
+             (hj,typ_cl) p)
+    with _ -> anomaly "apply_coercion"
+
+  let inh_app_fun env isevars j = 
+    let t = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+      match kind_of_term t with
+	| Prod (_,_,_) -> (isevars,j)
+	| Evar ev when not (is_defined_evar isevars ev) ->
+	    let (isevars',t) = define_evar_as_arrow isevars ev in
+	      (isevars',{ uj_val = j.uj_val; uj_type = t })
+	| _ ->
+       	    (try
+ 	       let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      	       let p = lookup_path_to_fun_from i1 in
+		 (isevars,apply_coercion env p j t)
+	     with Not_found -> (isevars,j))
+
+  let inh_tosort_force loc env isevars j =
+    try
+      let t,i1 = class_of1 env (evars_of isevars) j.uj_type in
+      let p = lookup_path_to_sort_from i1 in
+      let j1 = apply_coercion env p j t in 
+	(isevars,type_judgment env (j_nf_evar (evars_of isevars) j1))
+    with Not_found ->
+      error_not_a_type_loc loc env (evars_of isevars) j
+
+  let inh_coerce_to_sort loc env isevars j =
+    let typ = whd_betadeltaiota env (evars_of isevars) j.uj_type in
+      match kind_of_term typ with
+	| Sort s -> (isevars,{ utj_val = j.uj_val; utj_type = s })
+	| Evar ev when not (is_defined_evar isevars ev) ->
+	    let (isevars',s) = define_evar_as_sort isevars ev in
+	      (isevars',{ utj_val = j.uj_val; utj_type = s })
+	| _ ->
+	    inh_tosort_force loc env isevars j
+
+  let inh_coerce_to_fail env isevars c1 hj =
+    let hj' =
+      try 
+	let t1,i1 = class_of1 env (evars_of isevars) c1 in
+	let t2,i2 = class_of1 env (evars_of isevars) hj.uj_type in
+	let p = lookup_path_between (i2,i1) in
+	  apply_coercion env p hj t2
+      with Not_found -> raise NoCoercion 
+    in
+      try (the_conv_x_leq env hj'.uj_type c1 isevars, hj')
+      with Reduction.NotConvertible -> raise NoCoercion
+
+  let rec inh_conv_coerce_to_fail env isevars hj c1 =
+    let {uj_val = v; uj_type = t} = hj in
+      try (the_conv_x_leq env t c1 isevars, hj)
+      with Reduction.NotConvertible ->
+	(try 
+	   inh_coerce_to_fail env isevars c1 hj
+	 with NoCoercion ->
+	   (match kind_of_term (whd_betadeltaiota env (evars_of isevars) t),
+	      kind_of_term (whd_betadeltaiota env (evars_of isevars) c1) with
+		| Prod (_,t1,t2), Prod (name,u1,u2) -> 
+		    let v' = whd_betadeltaiota env (evars_of isevars) v in
+		    let (evd',b) =
+		      match kind_of_term v' with
+			| Lambda (_,v1,v2) ->
+			    (try the_conv_x env v1 u1 isevars, true  (* leq v1 u1? *)
+			     with Reduction.NotConvertible -> (isevars, false))
+			| _  -> (isevars,false) in
+		      if b
+		      then 
+			let (x,v1,v2) = destLambda v' in
+			let env1 = push_rel (x,None,v1) env in
+			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
 			  {uj_val = v2; uj_type = t2 } u2 in
-               (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
-                 uj_type = mkProd (x, v1, h2.uj_type) })
-             else 
-               (* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
-               (* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
-               (* has type (name:u1)u2 (with v' recursively obtained) *)
-               let name = (match name with 
-			     | Anonymous -> Name (id_of_string "x")
-                             | _ -> name) in
-               let env1 = push_rel (name,None,u1) env in
-               let (evd',h1) =
-		 inh_conv_coerce_to_fail env1 isevars
-		   {uj_val = mkRel 1; uj_type = (lift 1 u1) }
-                   (lift 1 t1) in
-               let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
-			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
-                           uj_type = subst1 h1.uj_val t2 }
+			  (evd'',{ uj_val = mkLambda (x, v1, h2.uj_val);
+				   uj_type = mkProd (x, v1, h2.uj_type) })
+		      else 
+			(* Mismatch on t1 and u1 or not a lambda: we eta-expand *)
+			(* we look for a coercion c:u1->t1 s.t. [name:u1](v' (c x)) *)
+			(* has type (name:u1)u2 (with v' recursively obtained) *)
+			let name = (match name with 
+				      | Anonymous -> Name (id_of_string "x")
+				      | _ -> name) in
+			let env1 = push_rel (name,None,u1) env in
+			let (evd',h1) =
+			  inh_conv_coerce_to_fail env1 isevars
+			    {uj_val = mkRel 1; uj_type = (lift 1 u1) }
+			    (lift 1 t1) in
+			let (evd'',h2) = inh_conv_coerce_to_fail env1 evd'
+			  { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
+                            uj_type = subst1 h1.uj_val t2 }
                           u2
-	       in
-               (evd'',
-                { uj_val = mkLambda (name, u1, h2.uj_val);
-                  uj_type = mkProd (name, u1, h2.uj_type) })
-	 | _ -> raise NoCoercion))
-
-(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-let inh_conv_coerce_to loc env isevars cj t =
-  let (evd',cj') = 
-    try 
-      inh_conv_coerce_to_fail env isevars cj t
-    with NoCoercion ->
-      let sigma = evars_of isevars in
-      error_actual_type_loc loc env sigma cj t
-  in
-  (evd',{ uj_val = cj'.uj_val; uj_type = t })
+			in
+			  (evd'',
+			   { uj_val = mkLambda (name, u1, h2.uj_val);
+			     uj_type = mkProd (name, u1, h2.uj_type) })
+		| _ -> raise NoCoercion))
+
+  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
+  let inh_conv_coerce_to loc env isevars cj t =
+    let (evd',cj') = 
+      try 
+	inh_conv_coerce_to_fail env isevars cj t
+      with NoCoercion ->
+	let sigma = evars_of isevars in
+	  error_actual_type_loc loc env sigma cj t
+    in
+      (evd',{ uj_val = cj'.uj_val; uj_type = t })
+end
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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index df76f992d0..14326bf449 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,27 +28,12 @@ open Evarutil
 open Pretype_errors
 open Rawterm
 open Evarconv
-open Coercion
 open Pattern
 open Dyn
 
-
-let evd_comb0 f isevars =
-  let (evd',x) = f !isevars in
-  isevars := evd';
-  x
-let evd_comb1 f isevars x =
-  let (evd',y) = f !isevars x in
-  isevars := evd';
-  y
-let evd_comb2 f isevars x y =
-  let (evd',z) = f !isevars x y in
-  isevars := evd';
-  z
-let evd_comb3 f isevars x y z =
-  let (evd',t) = f !isevars x y z in
-  isevars := evd';
-  t
+type typing_constraint = OfType of types option | IsType
+type var_map = (identifier * unsafe_judgment) list
+type unbound_ltac_var_map = (identifier * identifier option) list
 
 (************************************************************************)
 (* This concerns Cases *)
@@ -62,513 +47,613 @@ open Inductiveops
 let ((constr_in : constr -> Dyn.t),
      (constr_out : Dyn.t -> constr)) = create "constr"
 
-let mt_evd = Evd.empty
-
-let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
-
-(* Utilisé pour inférer le prédicat des Cases *)
-(* Semble exagérement fort *)
-(* Faudra préférer une unification entre les types de toutes les clauses *)
-(* et autoriser des ? à rester dans le résultat de l'unification *)
-
-let evar_type_fixpoint loc env isevars lna lar vdefj =
-  let lt = Array.length vdefj in 
-    if Array.length lar = lt then 
-      for i = 0 to lt-1 do 
-        if not (e_cumul env isevars (vdefj.(i)).uj_type
-		  (lift lt lar.(i))) then
-          error_ill_typed_rec_body_loc loc env (evars_of !isevars)
-            i lna vdefj lar
-      done
-
-let check_branches_message loc env isevars c (explft,lft) = 
-  for i = 0 to Array.length explft - 1 do
-    if not (e_cumul env isevars lft.(i) explft.(i)) then 
-      let sigma = evars_of !isevars in
-      error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
-  done
-
-(* coerce to tycon if any *)
-let inh_conv_coerce_to_tycon loc env isevars j = function
-   | None -> j
-   | Some typ -> evd_comb2 (inh_conv_coerce_to loc env) isevars j typ
-
-let push_rels vars env = List.fold_right push_rel vars env
-
-(*
-let evar_type_case isevars env ct pt lft p c =
-  let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
-  in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
-*)
-
-let strip_meta id = (* For Grammar v7 compatibility *)
-  let s = string_of_id id in
-  if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
-  else id
-
-let pretype_id loc env (lvar,unbndltacvars) id =
-  let id = strip_meta id in (* May happen in tactics defined by Grammar *)
-  try
-    let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
-  with Not_found ->
-  try
-    List.assoc id lvar
-  with Not_found ->
-  try
-    let (_,_,typ) = lookup_named id env in
-    { uj_val  = mkVar id; uj_type = typ }
-  with Not_found ->
-  try (* To build a nicer ltac error message *)
-    match List.assoc id unbndltacvars with
-      | None -> user_err_loc (loc,"",
-	str "variable " ++ pr_id id ++ str " should be bound to a term")
-      | Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
-  with Not_found ->
-    error_var_not_found_loc loc id
-
-(* make a dependent predicate from an undependent one *)
-
-let make_dep_of_undep env (IndType (indf,realargs)) pj =
-  let n = List.length realargs in
-  let rec decomp n p =
-    if n=0 then p else
-      match kind_of_term p with
-	| Lambda (_,_,c) -> decomp (n-1) c
-	| _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) 
-  in
-  let sign,s = decompose_prod_n n pj.uj_type in
-  let ind = build_dependent_inductive env indf in
-  let s' = mkProd (Anonymous, ind, s) in
-  let ccl = lift 1 (decomp n pj.uj_val) in
-  let ccl' = mkLambda (Anonymous, ind, ccl) in
-  {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
-
-(*************************************************************************)
-(* Main pretyping function                                               *)
-
-let pretype_ref isevars env ref = 
-  let c = constr_of_global ref in
-  make_judge c (Retyping.get_type_of env Evd.empty c)
-
-let pretype_sort = function
-  | RProp c -> judge_of_prop_contents c
-  | RType _ -> judge_of_new_Type ()
-
-(* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
-(* in environment [env], with existential variables [(evars_of isevars)] and *)
-(* the type constraint tycon *)
-let rec pretype tycon env isevars lvar = function
-
-  | RRef (loc,ref) ->
-      inh_conv_coerce_to_tycon loc env isevars
-	(pretype_ref isevars env ref)
-	tycon
-
-  | RVar (loc, id) ->
-      inh_conv_coerce_to_tycon loc env isevars
-	(pretype_id loc env lvar id)
-	tycon
-
-  | REvar (loc, ev, instopt) ->
-      (* Ne faudrait-il pas s'assurer que hyps est bien un
-      sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
-      let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
-      let args = match instopt with
-        | None -> instance_from_named_context hyps
-        | Some inst -> failwith "Evar subtitutions not implemented" in
-      let c = mkEvar (ev, args) in
-      let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
-      inh_conv_coerce_to_tycon loc env isevars j tycon
-
-  | RPatVar (loc,(someta,n)) -> 
-      anomaly "Found a pattern variable in a rawterm to type"
-	   
-  | RHole (loc,k) ->
-      let ty =
-        match tycon with 
-          | Some ty -> ty
-          | None ->
-              e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
-      { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
-
-  | RRec (loc,fixkind,names,bl,lar,vdef) ->
-      let rec type_bl env ctxt = function
-          [] -> ctxt
-        | (na,None,ty)::bl ->
-            let ty' = pretype_type empty_valcon env isevars lvar ty in
-            let dcl = (na,None,ty'.utj_val) in
-            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
-        | (na,Some bd,ty)::bl ->
-            let ty' = pretype_type empty_valcon env isevars lvar ty in
-            let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
-            let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
-            type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
-      let ctxtv = Array.map (type_bl env empty_rel_context) bl in
-      let larj =
-        array_map2
-          (fun e ar ->
-            pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
-          ctxtv lar in
-      let lara = Array.map (fun a -> a.utj_val) larj in
-      let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
-      let nbfix = Array.length lar in
-      let names = Array.map (fun id -> Name id) names in
-      (* Note: bodies are not used by push_rec_types, so [||] is safe *)
-      let newenv = push_rec_types (names,ftys,[||]) env in
-      let vdefj =
-	array_map2_i 
-	  (fun i ctxt def ->
-            (* we lift nbfix times the type in tycon, because of
-	     * the nbfix variables pushed to newenv *)
-            let (ctxt,ty) =
-              decompose_prod_n_assum (rel_context_length ctxt)
-                (lift nbfix ftys.(i)) in
-            let nenv = push_rel_context ctxt newenv in
-            let j = pretype (mk_tycon ty) nenv isevars lvar def in
-            { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
-              uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
-          ctxtv vdef in
-      evar_type_fixpoint loc env isevars names ftys vdefj;
-      let fixj =
-	match fixkind with
-	  | RFix (vn,i) ->
-	      let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
-	      (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkFix fix) ftys.(i)
-	  | RCoFix i -> 
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
-	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
-	      make_judge (mkCoFix cofix) ftys.(i) in
-      inh_conv_coerce_to_tycon loc env isevars fixj tycon
-
-  | RSort (loc,s) ->
-      inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
-
-  | RApp (loc,f,args) -> 
-      let fj = pretype empty_tycon env isevars lvar f in
-      let floc = loc_of_rawconstr f in
-      let rec apply_rec env n resj = function
-	| [] -> resj
-	| c::rest ->
-	    let argloc = loc_of_rawconstr c in
-	    let resj = evd_comb1 (inh_app_fun env) isevars resj in
-            let resty =
-              whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
-      	    match kind_of_term resty with
-	      | Prod (na,c1,c2) ->
-		  let hj = pretype (mk_tycon c1) env isevars lvar c in
-		  let newresj =
-      		    { uj_val = applist (j_val resj, [j_val hj]);
-		      uj_type = subst1 hj.uj_val c2 } in
-		  apply_rec env (n+1) newresj rest
-
-	      | _ ->
-		  let hj = pretype empty_tycon env isevars lvar c in
-		  error_cant_apply_not_functional_loc 
-		    (join_loc floc argloc) env (evars_of !isevars)
-	      	    resj [hj]
-
-      in let resj = apply_rec env 1 fj args in
-      (*
-	let apply_one_arg (floc,tycon,jl) c =
-	let (dom,rng) = split_tycon floc env isevars tycon in
-	let cj = pretype dom env isevars lvar c in
-	let rng_tycon =
-	  option_app (subst1 cj.uj_val) rng in
-	let argloc = loc_of_rawconstr c in
-	(join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
-	let _,_,jl =
-	List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in
-	let jl = List.rev jl in
-	let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in
-      *)
-      inh_conv_coerce_to_tycon loc env isevars resj tycon
-
-  | RLambda(loc,name,c1,c2)      ->
-      let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
-      let dom_valcon = valcon_of_tycon dom in
-      let j = pretype_type dom_valcon env isevars lvar c1 in
-      let var = (name,None,j.utj_val) in
-      let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-      judge_of_abstraction env name j j'
-
-  | RProd(loc,name,c1,c2)        ->
-      let j = pretype_type empty_valcon env isevars lvar c1 in
-      let var = (name,j.utj_val) in
-      let env' = push_rel_assum var env in
-      let j' = pretype_type empty_valcon env' isevars lvar c2 in
-      let resj =
-	try judge_of_product env name j j'
-	with TypeError _ as e -> Stdpp.raise_with_loc loc e in
-      inh_conv_coerce_to_tycon loc env isevars resj tycon
+(** Miscellaneous interpretation functions *)
+  
+let interp_sort = function
+  | RProp c -> Prop c
+  | RType _ -> new_Type_sort ()
+      
+let interp_elimination_sort = function
+  | RProp Null -> InProp
+  | RProp Pos  -> InSet
+  | RType _ -> InType
+
+module type S = 
+sig
+
+  module Cases : Cases.S
+  
+  (* Generic call to the interpreter from rawconstr to open_constr, leaving
+     unresolved holes as evars and returning the typing contexts of
+     these evars. Work as [understand_gen] for the rest. *)
+  
+  val understand_tcc :
+    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    
+  (* More general entry point with evars from ltac *)
+    
+  (* Generic call to the interpreter from rawconstr to constr, failing
+     unresolved holes in the rawterm cannot be instantiated.
+     
+     In [understand_ltac sigma env ltac_env constraint c],
+     
+     sigma : initial set of existential variables (typically dependent subgoals)
+     ltac_env : partial substitution of variables (used for the tactic language)
+     constraint : tell if interpreted as a possibly constrained term or a type 
+  *)
+    
+  val understand_ltac :
+    evar_map -> env -> var_map * unbound_ltac_var_map ->
+    typing_constraint -> rawconstr -> evar_defs * constr
+    
+  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+    
+  val understand : evar_map -> env -> ?expected_type:Term.types ->
+    rawconstr -> constr
+    
+  (* Idem but the rawconstr is intended to be a type *)
+    
+  val understand_type : evar_map -> env -> rawconstr -> constr
+    
+  (* A generalization of the two previous case *)
+    
+  val understand_gen : typing_constraint -> evar_map -> env -> 
+    rawconstr -> constr
+    
+  (* Idem but returns the judgment of the understood term *)
+    
+  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+
+  (* Idem but do not fail on unresolved evars *)
+
+  val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+
+  (*i*)
+  (* Internal of Pretyping...
+   * Unused outside, but useful for debugging
+   *)
+  val pretype : 
+    type_constraint -> env -> evar_defs ref -> 
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_judgment
+    
+  val pretype_type : 
+    val_constraint -> env -> evar_defs ref ->
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_type_judgment
+
+  val pretype_gen :
+    evar_defs ref -> env -> 
+    var_map * (identifier * identifier option) list ->
+    typing_constraint -> rawconstr -> constr
+
+    (*i*)
+end
+
+module Pretyping_F (Coercion : Coercion.S) = struct
+
+  module Cases = Cases.Cases_F(Coercion)
+
+  let evd_comb0 f isevars =
+    let (evd',x) = f !isevars in
+      isevars := evd';
+      x
+
+  let evd_comb1 f isevars x =
+    let (evd',y) = f !isevars x in
+      isevars := evd';
+      y
+
+  let evd_comb2 f isevars x y =
+    let (evd',z) = f !isevars x y in
+      isevars := evd';
+      z
+
+  let evd_comb3 f isevars x y z =
+    let (evd',t) = f !isevars x y z in
+      isevars := evd';
+      t
 	
-  | RLetIn(loc,name,c1,c2)      ->
-      let j = pretype empty_tycon env isevars lvar c1 in
-      let t = refresh_universes j.uj_type in
-      let var = (name,Some j.uj_val,t) in
-        let tycon = option_app (lift 1) tycon in
-      let j' = pretype tycon (push_rel var env) isevars lvar c2 in
-      { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
-	uj_type = subst1 j.uj_val j'.uj_type }
-
-  | RLetTuple (loc,nal,(na,po),c,d) ->
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs)) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
-	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
-      in
-      let cstrs = get_constructors env indf in
-      if Array.length cstrs <> 1 then
-        user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
-      let cs = cstrs.(0) in
-      if List.length nal <> cs.cs_nargs then
-        user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
-      let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
-        (List.rev nal) cs.cs_args in
-      let env_f = push_rels fsign env in
-      (* Make dependencies from arity signature impossible *)
-      let arsgn,_ = get_arity env indf in
-      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
-      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
-      let nar = List.length arsgn in
-      (match po with
-	 | Some p ->
-             let env_p = push_rels psign env in
-             let pj = pretype_type empty_valcon env_p isevars lvar p in
-             let ccl = nf_evar (evars_of !isevars) pj.utj_val in
-	     let psign = make_arity_signature env true indf in (* with names *)
-	     let p = it_mkLambda_or_LetIn ccl psign in
-             let inst = 
-	       (Array.to_list cs.cs_concl_realargs)
-	       @[build_dependent_constructor cs] in
-	     let lp = lift cs.cs_nargs p in
-             let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
-	     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
-	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env LetStyle mis in
-	       mkCase (ci, p, cj.uj_val,[|f|]) in 
-	     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
-
-	 | None -> 
-             let tycon = option_app (lift cs.cs_nargs) tycon in
-	     let fj = pretype tycon env_f isevars lvar d in
-	     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-	     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
-             let ccl =
-               if noccur_between 1 cs.cs_nargs ccl then
-                 lift (- cs.cs_nargs) ccl 
-               else
-                 error_cant_find_case_type_loc loc env (evars_of !isevars) 
-                   cj.uj_val in
-             let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env LetStyle mis in
-	       mkCase (ci, p, cj.uj_val,[|f|] ) 
-	     in
-	     { uj_val = v; uj_type = ccl })
-
-  | RIf (loc,c,(na,po),b1,b2) ->
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs)) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
+  let mt_evd = Evd.empty
+    
+  let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
+      
+  (* Utilisé pour inférer le prédicat des Cases *)
+  (* Semble exagérement fort *)
+  (* Faudra préférer une unification entre les types de toutes les clauses *)
+  (* et autoriser des ? à rester dans le résultat de l'unification *)
+  
+  let evar_type_fixpoint loc env isevars lna lar vdefj =
+    let lt = Array.length vdefj in 
+      if Array.length lar = lt then 
+	for i = 0 to lt-1 do 
+          if not (e_cumul env isevars (vdefj.(i)).uj_type
+		    (lift lt lar.(i))) then
+            error_ill_typed_rec_body_loc loc env (evars_of !isevars)
+              i lna vdefj lar
+	done
+
+  let check_branches_message loc env isevars c (explft,lft) = 
+    for i = 0 to Array.length explft - 1 do
+      if not (e_cumul env isevars lft.(i) explft.(i)) then 
+	let sigma = evars_of !isevars in
+	  error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i)
+    done
+
+  (* coerce to tycon if any *)
+  let inh_conv_coerce_to_tycon loc env isevars j = function
+    | None -> j
+    | Some typ -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) isevars j typ
+
+  let push_rels vars env = List.fold_right push_rel vars env
+
+  (*
+    let evar_type_case isevars env ct pt lft p c =
+    let (mind,bty,rslty) = type_case_branches env (evars_of isevars) ct pt p c
+    in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
+  *)
+
+  let strip_meta id = (* For Grammar v7 compatibility *)
+    let s = string_of_id id in
+      if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+      else id
+
+  let pretype_id loc env (lvar,unbndltacvars) id =
+    let id = strip_meta id in (* May happen in tactics defined by Grammar *)
+      try
+	let (n,typ) = lookup_rel_id id (rel_context env) in
+	  { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
+      with Not_found ->
+	try
+	  List.assoc id lvar
 	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
-      let cstrs = get_constructors env indf in 
-      if Array.length cstrs <> 2 then
-        user_err_loc (loc,"",
-	  str "If is only for inductive types with two constructors");
-
-      (* Make dependencies from arity signature impossible *)
-      let arsgn,_ = get_arity env indf in
-      let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
-      let nar = List.length arsgn in
-      let psign = (na,None,build_dependent_inductive env indf)::arsgn in
-      let pred,p = match po with
-	| Some p ->
-	    let env_p = push_rels psign env in
-            let pj = pretype_type empty_valcon env_p isevars lvar p in
-            let ccl = nf_evar (evars_of !isevars) pj.utj_val in
-	    let pred = it_mkLambda_or_LetIn ccl psign in
-	    pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
-	| None -> 
-	    let p = match tycon with
-	    | Some ty -> ty
-	    | None ->
-                e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
-	    in
-	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-      let f cs b =
-	let n = rel_context_length cs.cs_args in
-	let pi = liftn n 2 pred in
-	let pi = beta_applist (pi, [build_dependent_constructor cs]) in
-	let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in
-	let env_c = push_rels csgn env in 
-	let bj = pretype (Some pi) env_c isevars lvar b in
-	it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
-      let b1 = f cstrs.(0) b1 in
-      let b2 = f cstrs.(1) b2 in
-      let pred = nf_evar (evars_of !isevars) pred in
-      let p = nf_evar (evars_of !isevars) p in
-      let v =
-	let mis,_ = dest_ind_family indf in
-	let ci = make_default_case_info env IfStyle mis in
-	mkCase (ci, pred, cj.uj_val, [|b1;b2|])
-      in
-      { uj_val = v; uj_type = p }
-
-  | RCases (loc,po,tml,eqns) ->
-      Cases.compile_cases loc
-	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
-	tycon env (* loc *) (po,tml,eqns)
-
-  | RCast(loc,c,k,t) ->
-      let tj = pretype_type empty_tycon env isevars lvar t in
-      let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
-      (* User Casts are for helping pretyping, experimentally not to be kept*)
-      (* ... except for Correctness *)
-      let v = mkCast (cj.uj_val, k, tj.utj_val) in
-      let cj = { uj_val = v; uj_type = tj.utj_val } in
-      inh_conv_coerce_to_tycon loc env isevars cj tycon
-
-  | RDynamic (loc,d) ->
-    if (tag d) = "constr" then
-      let c = constr_out d in
-      let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	  try
+	    let (_,_,typ) = lookup_named id env in
+	      { uj_val  = mkVar id; uj_type = typ }
+	  with Not_found ->
+	    try (* To build a nicer ltac error message *)
+	      match List.assoc id unbndltacvars with
+		| None -> user_err_loc (loc,"",
+					str "variable " ++ pr_id id ++ str " should be bound to a term")
+		| Some id0 -> Pretype_errors.error_var_not_found_loc loc id0
+	    with Not_found ->
+	      error_var_not_found_loc loc id
+
+  (* make a dependent predicate from an undependent one *)
+
+  let make_dep_of_undep env (IndType (indf,realargs)) pj =
+    let n = List.length realargs in
+    let rec decomp n p =
+      if n=0 then p else
+	match kind_of_term p with
+	  | Lambda (_,_,c) -> decomp (n-1) c
+	  | _ -> decomp (n-1) (applist (lift 1 p, [mkRel 1])) 
+    in
+    let sign,s = decompose_prod_n n pj.uj_type in
+    let ind = build_dependent_inductive env indf in
+    let s' = mkProd (Anonymous, ind, s) in
+    let ccl = lift 1 (decomp n pj.uj_val) in
+    let ccl' = mkLambda (Anonymous, ind, ccl) in
+      {uj_val=lam_it ccl' sign; uj_type=prod_it s' sign} 
+
+  (*************************************************************************)
+  (* Main pretyping function                                               *)
+
+  let pretype_ref isevars env ref = 
+    let c = constr_of_global ref in
+      make_judge c (Retyping.get_type_of env Evd.empty c)
+
+  let pretype_sort = function
+    | RProp c -> judge_of_prop_contents c
+    | RType _ -> judge_of_new_Type ()
+
+  (* [pretype tycon env isevars lvar lmeta cstr] attempts to type [cstr] *)
+  (* in environment [env], with existential variables [(evars_of isevars)] and *)
+  (* the type constraint tycon *)
+  let rec pretype tycon env isevars lvar = function
+
+    | RRef (loc,ref) ->
+	inh_conv_coerce_to_tycon loc env isevars
+	  (pretype_ref isevars env ref)
+	  tycon
+
+    | RVar (loc, id) ->
+	inh_conv_coerce_to_tycon loc env isevars
+	  (pretype_id loc env lvar id)
+	  tycon
+
+    | REvar (loc, ev, instopt) ->
+	(* Ne faudrait-il pas s'assurer que hyps est bien un
+	   sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
+	let hyps = evar_context (Evd.map (evars_of !isevars) ev) in
+	let args = match instopt with
+          | None -> instance_from_named_context hyps
+          | Some inst -> failwith "Evar subtitutions not implemented" in
+	let c = mkEvar (ev, args) in
+	let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	  inh_conv_coerce_to_tycon loc env isevars j tycon
+
+    | RPatVar (loc,(someta,n)) -> 
+	anomaly "Found a pattern variable in a rawterm to type"
+	  
+    | RHole (loc,k) ->
+	let ty =
+          match tycon with 
+            | Some ty -> ty
+            | None ->
+		e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ()) in
+	  { uj_val = e_new_evar isevars env ~src:(loc,k) ty; uj_type = ty }
+
+    | RRec (loc,fixkind,names,bl,lar,vdef) ->
+	let rec type_bl env ctxt = function
+            [] -> ctxt
+          | (na,None,ty)::bl ->
+              let ty' = pretype_type empty_valcon env isevars lvar ty in
+              let dcl = (na,None,ty'.utj_val) in
+		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+          | (na,Some bd,ty)::bl ->
+              let ty' = pretype_type empty_valcon env isevars lvar ty in
+              let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in
+              let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
+		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+	let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+	let larj =
+          array_map2
+            (fun e ar ->
+               pretype_type empty_valcon (push_rel_context e env) isevars lvar ar)
+            ctxtv lar in
+	let lara = Array.map (fun a -> a.utj_val) larj in
+	let ftys = array_map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in
+	let nbfix = Array.length lar in
+	let names = Array.map (fun id -> Name id) names in
+	  (* Note: bodies are not used by push_rec_types, so [||] is safe *)
+	let newenv = push_rec_types (names,ftys,[||]) env in
+	let vdefj =
+	  array_map2_i 
+	    (fun i ctxt def ->
+               (* we lift nbfix times the type in tycon, because of
+		* the nbfix variables pushed to newenv *)
+               let (ctxt,ty) =
+		 decompose_prod_n_assum (rel_context_length ctxt)
+                   (lift nbfix ftys.(i)) in
+               let nenv = push_rel_context ctxt newenv in
+               let j = pretype (mk_tycon ty) nenv isevars lvar def in
+		 { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt;
+		   uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
+            ctxtv vdef in
+	  evar_type_fixpoint loc env isevars names ftys vdefj;
+	  let fixj =
+	    match fixkind with
+	      | RFix (vn,i) ->
+		  let fix = ((Array.map fst vn, i),(names,ftys,Array.map j_val vdefj)) in
+		    (try check_fix env fix with e -> Stdpp.raise_with_loc loc e);
+		    make_judge (mkFix fix) ftys.(i)
+	      | RCoFix i -> 
+		  let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+		    (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
+		    make_judge (mkCoFix cofix) ftys.(i) in
+	    inh_conv_coerce_to_tycon loc env isevars fixj tycon
+
+    | RSort (loc,s) ->
+	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
+
+    | RApp (loc,f,args) -> 
+	let fj = pretype empty_tycon env isevars lvar f in
+	let floc = loc_of_rawconstr f in
+	let rec apply_rec env n resj = function
+	  | [] -> resj
+	  | c::rest ->
+	      let argloc = loc_of_rawconstr c in
+	      let resj = evd_comb1 (Coercion.inh_app_fun env) isevars resj in
+              let resty =
+		whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
+      		match kind_of_term resty with
+		  | Prod (na,c1,c2) ->
+		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      let newresj =
+      			{ uj_val = applist (j_val resj, [j_val hj]);
+			  uj_type = subst1 hj.uj_val c2 } in
+			apply_rec env (n+1) newresj rest
+
+		  | _ ->
+		      let hj = pretype empty_tycon env isevars lvar c in
+			error_cant_apply_not_functional_loc 
+			  (join_loc floc argloc) env (evars_of !isevars)
+	      		  resj [hj]
+
+	in let resj = apply_rec env 1 fj args in
+	  (*
+	    let apply_one_arg (floc,tycon,jl) c =
+	    let (dom,rng) = split_tycon floc env isevars tycon in
+	    let cj = pretype dom env isevars lvar c in
+	    let rng_tycon =
+	    option_app (subst1 cj.uj_val) rng in
+	    let argloc = loc_of_rawconstr c in
+	    (join_loc floc argloc,rng_tycon,(argloc,cj)::jl)  in
+	    let _,_,jl =
+	    List.fold_left apply_one_arg (floc,mk_tycon j.uj_type,[]) args in
+	    let jl = List.rev jl in
+	    let resj = inh_apply_rel_list loc env isevars jl (floc,j) tycon in
+	  *)
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+
+    | RLambda(loc,name,c1,c2)      ->
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	let dom_valcon = valcon_of_tycon dom in
+	let j = pretype_type dom_valcon env isevars lvar c1 in
+	let var = (name,None,j.utj_val) in
+	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
+	  judge_of_abstraction env name j j'
+
+    | RProd(loc,name,c1,c2)        ->
+	let j = pretype_type empty_valcon env isevars lvar c1 in
+	let var = (name,j.utj_val) in
+	let env' = push_rel_assum var env in
+	let j' = pretype_type empty_valcon env' isevars lvar c2 in
+	let resj =
+	  try judge_of_product env name j j'
+	  with TypeError _ as e -> Stdpp.raise_with_loc loc e in
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
+	    
+    | RLetIn(loc,name,c1,c2)      ->
+	let j = pretype empty_tycon env isevars lvar c1 in
+	let t = refresh_universes j.uj_type in
+	let var = (name,Some j.uj_val,t) in
+        let tycon = option_app (lift 1) tycon in
+	let j' = pretype tycon (push_rel var env) isevars lvar c2 in
+	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+	    uj_type = subst1 j.uj_val j'.uj_type }
+
+    | RLetTuple (loc,nal,(na,po),c,d) ->
+	let cj = pretype empty_tycon env isevars lvar c in
+	let (IndType (indf,realargs)) = 
+	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  with Not_found ->
+	    let cloc = loc_of_rawconstr c in
+	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
+	in
+	let cstrs = get_constructors env indf in
+	  if Array.length cstrs <> 1 then
+            user_err_loc (loc,"",str "Destructing let is only for inductive types with one constructor");
+	  let cs = cstrs.(0) in
+	    if List.length nal <> cs.cs_nargs then
+              user_err_loc (loc,"", str "Destructing let on this type expects " ++ int cs.cs_nargs ++ str " variables");
+	    let fsign = List.map2 (fun na (_,c,t) -> (na,c,t))
+              (List.rev nal) cs.cs_args in
+	    let env_f = push_rels fsign env in
+	      (* Make dependencies from arity signature impossible *)
+	    let arsgn,_ = get_arity env indf in
+	    let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+	    let nar = List.length arsgn in
+	      (match po with
+		 | Some p ->
+		     let env_p = push_rels psign env in
+		     let pj = pretype_type empty_valcon env_p isevars lvar p in
+		     let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+		     let psign = make_arity_signature env true indf in (* with names *)
+		     let p = it_mkLambda_or_LetIn ccl psign in
+		     let inst = 
+		       (Array.to_list cs.cs_concl_realargs)
+		       @[build_dependent_constructor cs] in
+		     let lp = lift cs.cs_nargs p in
+		     let fty = hnf_lam_applist env (evars_of !isevars) lp inst in
+		     let fj = pretype (mk_tycon fty) env_f isevars lvar d in
+		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		     let v =
+		       let mis,_ = dest_ind_family indf in
+		       let ci = make_default_case_info env LetStyle mis in
+			 mkCase (ci, p, cj.uj_val,[|f|]) in 
+		       { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+		 | None -> 
+		     let tycon = option_app (lift cs.cs_nargs) tycon in
+		     let fj = pretype tycon env_f isevars lvar d in
+		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		     let ccl = nf_evar (evars_of !isevars) fj.uj_type in
+		     let ccl =
+		       if noccur_between 1 cs.cs_nargs ccl then
+			 lift (- cs.cs_nargs) ccl 
+		       else
+			 error_cant_find_case_type_loc loc env (evars_of !isevars) 
+			   cj.uj_val in
+		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+		     let v =
+		       let mis,_ = dest_ind_family indf in
+		       let ci = make_default_case_info env LetStyle mis in
+			 mkCase (ci, p, cj.uj_val,[|f|] ) 
+		     in
+		       { uj_val = v; uj_type = ccl })
+
+    | RIf (loc,c,(na,po),b1,b2) ->
+	let cj = pretype empty_tycon env isevars lvar c in
+	let (IndType (indf,realargs)) = 
+	  try find_rectype env (evars_of !isevars) cj.uj_type
+	  with Not_found ->
+	    let cloc = loc_of_rawconstr c in
+	      error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
+	let cstrs = get_constructors env indf in 
+	  if Array.length cstrs <> 2 then
+            user_err_loc (loc,"",
+			  str "If is only for inductive types with two constructors");
+
+	  (* Make dependencies from arity signature impossible *)
+	  let arsgn,_ = get_arity env indf in
+	  let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+	  let nar = List.length arsgn in
+	  let psign = (na,None,build_dependent_inductive env indf)::arsgn in
+	  let pred,p = match po with
+	    | Some p ->
+		let env_p = push_rels psign env in
+		let pj = pretype_type empty_valcon env_p isevars lvar p in
+		let ccl = nf_evar (evars_of !isevars) pj.utj_val in
+		let pred = it_mkLambda_or_LetIn ccl psign in
+		  pred, lift (- nar) (beta_applist (pred,[cj.uj_val]))
+	    | None -> 
+		let p = match tycon with
+		  | Some ty -> ty
+		  | None ->
+                      e_new_evar isevars env ~src:(loc,InternalHole) (new_Type ())
+		in
+		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+	  let f cs b =
+	    let n = rel_context_length cs.cs_args in
+	    let pi = liftn n 2 pred in
+	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
+	    let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in
+	    let env_c = push_rels csgn env in 
+	    let bj = pretype (Some pi) env_c isevars lvar b in
+	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
+	  let b1 = f cstrs.(0) b1 in
+	  let b2 = f cstrs.(1) b2 in
+	  let pred = nf_evar (evars_of !isevars) pred in
+	  let p = nf_evar (evars_of !isevars) p in
+	  let v =
+	    let mis,_ = dest_ind_family indf in
+	    let ci = make_default_case_info env IfStyle mis in
+	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
+	  in
+	    { uj_val = v; uj_type = p }
+
+    | RCases (loc,po,tml,eqns) ->
+	Cases.compile_cases loc
+	  ((fun vtyc env -> pretype vtyc env isevars lvar),isevars)
+	  tycon env (* loc *) (po,tml,eqns)
+
+    | RCast(loc,c,k,t) ->
+	let tj = pretype_type empty_tycon env isevars lvar t in
+	let cj = pretype (mk_tycon tj.utj_val) env isevars lvar c in
+	  (* User Casts are for helping pretyping, experimentally not to be kept*)
+	  (* ... except for Correctness *)
+	let v = mkCast (cj.uj_val, k, tj.utj_val) in
+	let cj = { uj_val = v; uj_type = tj.utj_val } in
+	  inh_conv_coerce_to_tycon loc env isevars cj tycon
+
+    | RDynamic (loc,d) ->
+	if (tag d) = "constr" then
+	  let c = constr_out d in
+	  let j = (Retyping.get_judgment_of env (evars_of !isevars) c) in
+	    j
+	      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
+	else
+	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
+
+  (* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
+  and pretype_type valcon env isevars lvar = function
+    | RHole loc ->
+	(match valcon with
+	   | Some v ->
+               let s =
+		 let sigma = evars_of !isevars in
+		 let t = Retyping.get_type_of env sigma v in
+		   match kind_of_term (whd_betadeltaiota env sigma t) with
+                     | Sort s -> s
+                     | Evar v when is_Type (existential_type sigma v) -> 
+			 evd_comb1 (define_evar_as_sort) isevars v
+                     | _ -> anomaly "Found a type constraint which is not a type"
+               in
+		 { utj_val = v;
+		   utj_type = s }
+	   | None ->
+	       let s = new_Type_sort () in
+		 { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
+		   utj_type = s})
+    | c ->
+	let j = pretype empty_tycon env isevars lvar c in
+	let loc = loc_of_rawconstr c in
+	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) isevars j in
+	  match valcon with
+	    | None -> tj
+	    | Some v ->
+		if e_cumul env isevars v tj.utj_val then tj
+		else
+		  error_unexpected_type_loc
+                    (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
+
+  let pretype_gen isevars env lvar kind c =
+    let c' = match kind with
+      | OfType exptyp ->
+	  let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
+	    (pretype tycon env isevars lvar c).uj_val
+      | IsType ->
+	  (pretype_type empty_valcon env isevars lvar c).utj_val in
+      nf_evar (evars_of !isevars) c'
+
+  (* [check_evars] fails if some unresolved evar remains *)
+  (* it assumes that the defined existentials have already been substituted
+     (should be done in unsafe_infer and unsafe_infer_type) *)
+
+  let check_evars env initial_sigma isevars c =
+    let sigma = evars_of !isevars in
+    let rec proc_rec c =
+      match kind_of_term c with
+	| Evar (ev,args) ->
+            assert (Evd.in_dom sigma ev);
+	    if not (Evd.in_dom initial_sigma ev) then
+              let (loc,k) = evar_source ev !isevars in
+		error_unsolvable_implicit loc env sigma k
+	| _ -> iter_constr proc_rec c
+    in
+      proc_rec c(*;
+		  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
+		  if pbs <> [] then begin
+		  pperrnl
+		  (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
+		  prlist_with_sep fnl
+		  (fun  (pb,c1,c2) ->
+		  Termops.print_constr c1 ++
+		  (if pb=Reduction.CUMUL then str " <="++ spc()
+		  else str" =="++spc()) ++
+		  Termops.print_constr c2)
+		  pbs ++ fnl())
+		  end*)
+
+  (* TODO: comment faire remonter l'information si le typage a resolu des
+     variables du sigma original. il faudrait que la fonction de typage
+     retourne aussi le nouveau sigma...
+  *)
+
+  let understand_judgment sigma env c =
+    let isevars = ref (create_evar_defs sigma) in
+    let j = pretype empty_tycon env isevars ([],[]) c in
+    let j = j_nf_evar (evars_of !isevars) j in
+      check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
       j
-      (*inh_conv_coerce_to_tycon loc env isevars j tycon*)
-    else
-      user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic"))
-
-(* [pretype_type valcon env isevars lvar c] coerces [c] into a type *)
-and pretype_type valcon env isevars lvar = function
-  | RHole loc ->
-      (match valcon with
-	 | Some v ->
-             let s =
-               let sigma = evars_of !isevars in
-               let t = Retyping.get_type_of env sigma v in
-               match kind_of_term (whd_betadeltaiota env sigma t) with
-                 | Sort s -> s
-                 | Evar v when is_Type (existential_type sigma v) -> 
-                     evd_comb1 (define_evar_as_sort) isevars v
-                 | _ -> anomaly "Found a type constraint which is not a type"
-             in
-	     { utj_val = v;
-	       utj_type = s }
-	 | None ->
-	     let s = new_Type_sort () in
-	     { utj_val = e_new_evar isevars env ~src:loc (mkSort s);
-	       utj_type = s})
-  | c ->
-      let j = pretype empty_tycon env isevars lvar c in
-      let loc = loc_of_rawconstr c in
-      let tj = evd_comb1 (inh_coerce_to_sort loc env) isevars j in
-      match valcon with
-	| None -> tj
-	| Some v ->
-	    if e_cumul env isevars v tj.utj_val then tj
-	    else
-	      error_unexpected_type_loc
-                (loc_of_rawconstr c) env (evars_of !isevars) tj.utj_val v
 
+  let understand_judgment_tcc sigma env c =
+    let isevars = ref (create_evar_defs sigma) in
+    let j = pretype empty_tycon env isevars ([],[]) c in
+    let sigma = evars_of !isevars in
+    let j = j_nf_evar sigma j in
+      sigma, j
 
-type typing_constraint = OfType of types option | IsType
-
-let pretype_gen isevars env lvar kind c =
-  let c' = match kind with
-  | OfType exptyp ->
-    let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
-    (pretype tycon env isevars lvar c).uj_val
-  | IsType ->
-    (pretype_type empty_valcon env isevars lvar c).utj_val in
-  nf_evar (evars_of !isevars) c'
-
-(* [check_evars] fails if some unresolved evar remains *)
-(* it assumes that the defined existentials have already been substituted
-   (should be done in unsafe_infer and unsafe_infer_type) *)
-
-let check_evars env initial_sigma isevars c =
-  let sigma = evars_of !isevars in
-  let rec proc_rec c =
-    match kind_of_term c with
-      | Evar (ev,args) ->
-          assert (Evd.in_dom sigma ev);
-	  if not (Evd.in_dom initial_sigma ev) then
-            let (loc,k) = evar_source ev !isevars in
-	    error_unsolvable_implicit loc env sigma k
-      | _ -> iter_constr proc_rec c
-  in
-  proc_rec c(*;
-  let (_,pbs) = get_conv_pbs !isevars (fun _ -> true) in
-  if pbs <> [] then begin
-    pperrnl
-      (str"TYPING OF "++Termops.print_constr_env env c++fnl()++
-      prlist_with_sep fnl
-        (fun  (pb,c1,c2) ->
-          Termops.print_constr c1 ++
-          (if pb=Reduction.CUMUL then str " <="++ spc()
-           else str" =="++spc()) ++
-          Termops.print_constr c2)
-        pbs ++ fnl())
-  end*)
-
-(* TODO: comment faire remonter l'information si le typage a resolu des
-       variables du sigma original. il faudrait que la fonction de typage
-       retourne aussi le nouveau sigma...
-*)
-
-let understand_judgment sigma env c =
-  let isevars = ref (create_evar_defs sigma) in
-  let j = pretype empty_tycon env isevars ([],[]) c in
-  let j = j_nf_evar (evars_of !isevars) j in
-  check_evars env sigma isevars (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-  j
-
-(* Raw calls to the unsafe inference machine: boolean says if we must
-   fail on unresolved evars; the unsafe_judgment list allows us to
-   extend env with some bindings *)
-
-let ise_pretype_gen fail_evar sigma env lvar kind c =
-  let isevars = ref (create_evar_defs sigma) in
-  let c = pretype_gen isevars env lvar kind c in
-  if fail_evar then check_evars env sigma isevars c;
-  (!isevars, c)
-
-(** Entry points of the high-level type synthesis algorithm *)
+  (* Raw calls to the unsafe inference machine: boolean says if we must
+     fail on unresolved evars; the unsafe_judgment list allows us to
+     extend env with some bindings *)
 
-type var_map = (identifier * unsafe_judgment) list
-type unbound_ltac_var_map = (identifier * identifier option) list
+  let ise_pretype_gen fail_evar sigma env lvar kind c =
+    let isevars = ref (create_evar_defs sigma) in
+    let c = pretype_gen isevars env lvar kind c in
+      if fail_evar then check_evars env sigma isevars c;
+      (!isevars, c)
 
-let understand_gen kind sigma env c =
-  snd (ise_pretype_gen true sigma env ([],[]) kind c)
+  (** Entry points of the high-level type synthesis algorithm *)
 
-let understand sigma env ?expected_type:exptyp c =
-  snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
+  let understand_gen kind sigma env c =
+    snd (ise_pretype_gen true sigma env ([],[]) kind c)
 
-let understand_type sigma env c =
-  snd (ise_pretype_gen true sigma env ([],[]) IsType c)
+  let understand sigma env ?expected_type:exptyp c =
+    snd (ise_pretype_gen true sigma env ([],[]) (OfType exptyp) c)
 
-let understand_ltac sigma env lvar kind c =
-  ise_pretype_gen false sigma env lvar kind c
+  let understand_type sigma env c =
+    snd (ise_pretype_gen true sigma env ([],[]) IsType c)
 
-let understand_tcc sigma env ?expected_type:exptyp c =
-  let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
-  evars_of evars,c
+  let understand_ltac sigma env lvar kind c =
+    ise_pretype_gen false sigma env lvar kind c
 
-(** Miscellaneous interpretation functions *)
+  let understand_tcc sigma env ?expected_type:exptyp c =
+    let evars,c = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in
+      evars_of evars,c
+end
 
-let interp_sort = function
-  | RProp c -> Prop c
-  | RType _ -> new_Type_sort ()
-
-let interp_elimination_sort = function
-  | RProp Null -> InProp
-  | RProp Pos  -> InSet
-  | RType _ -> InType
+module Default : S = Pretyping_F(Coercion.Default)
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 8a7946cd72..f93e461298 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -20,70 +20,89 @@ open Evarutil
 
 type typing_constraint = OfType of types option | IsType
 
-(* Generic call to the interpreter from rawconstr to open_constr, leaving
-   unresolved holes as evars and returning the typing contexts of
-   these evars. Work as [understand_gen] for the rest. *)
-
-val understand_tcc :
-  evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
-
-(* More general entry point with evars from ltac *)
-
 type var_map = (identifier * unsafe_judgment) list
 type unbound_ltac_var_map = (identifier * identifier option) list
 
-(* Generic call to the interpreter from rawconstr to constr, failing
-   unresolved holes in the rawterm cannot be instantiated.
-
-   In [understand_ltac sigma env ltac_env constraint c],
-
-   sigma : initial set of existential variables (typically dependent subgoals)
-   ltac_env : partial substitution of variables (used for the tactic language)
-   constraint : tell if interpreted as a possibly constrained term or a type 
-*)
-
-val understand_ltac :
-  evar_map -> env -> var_map * unbound_ltac_var_map ->
+module type S = 
+sig
+
+  module Cases : Cases.S
+  
+  (* Generic call to the interpreter from rawconstr to open_constr, leaving
+     unresolved holes as evars and returning the typing contexts of
+     these evars. Work as [understand_gen] for the rest. *)
+  
+  val understand_tcc :
+    evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr
+    
+  (* More general entry point with evars from ltac *)
+    
+  (* Generic call to the interpreter from rawconstr to constr, failing
+     unresolved holes in the rawterm cannot be instantiated.
+     
+     In [understand_ltac sigma env ltac_env constraint c],
+     
+     sigma : initial set of existential variables (typically dependent subgoals)
+     ltac_env : partial substitution of variables (used for the tactic language)
+     constraint : tell if interpreted as a possibly constrained term or a type 
+  *)
+    
+  val understand_ltac :
+    evar_map -> env -> var_map * unbound_ltac_var_map ->
     typing_constraint -> rawconstr -> evar_defs * constr
+    
+  (* Standard call to get a constr from a rawconstr, resolving implicit args *)
+    
+  val understand : evar_map -> env -> ?expected_type:Term.types ->
+    rawconstr -> constr
+    
+  (* Idem but the rawconstr is intended to be a type *)
+    
+  val understand_type : evar_map -> env -> rawconstr -> constr
+    
+  (* A generalization of the two previous case *)
+    
+  val understand_gen : typing_constraint -> evar_map -> env -> 
+    rawconstr -> constr
+    
+  (* Idem but returns the judgment of the understood term *)
+    
+  val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+
+  (* Idem but do not fail on unresolved evars *)
+  val understand_judgment_tcc : evar_map -> env -> rawconstr -> evar_map * unsafe_judgment
+
+       
+  (*i*)
+  (* Internal of Pretyping...
+   *)
+  val pretype : 
+    type_constraint -> env -> evar_defs ref -> 
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_judgment
+    
+  val pretype_type : 
+    val_constraint -> env -> evar_defs ref ->
+    var_map * (identifier * identifier option) list ->
+    rawconstr -> unsafe_type_judgment
 
-(* Standard call to get a constr from a rawconstr, resolving implicit args *)
-
-val understand : evar_map -> env -> ?expected_type:Term.types ->
-  rawconstr -> constr
-
-(* Idem but the rawconstr is intended to be a type *)
-
-val understand_type : evar_map -> env -> rawconstr -> constr
-
-(* A generalization of the two previous case *)
-
-val understand_gen : typing_constraint -> evar_map -> env -> 
-  rawconstr -> constr
+  val pretype_gen :
+    evar_defs ref -> env -> 
+    var_map * (identifier * identifier option) list ->
+    typing_constraint -> rawconstr -> constr
 
-(* Idem but returns the judgment of the understood term *)
+  (*i*)
+    
+end
 
-val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment
+module Pretyping_F (C : Coercion.S) : S
+module Default : S
 
 (* To embed constr in rawconstr *)
-
+  
 val constr_in : constr -> Dyn.t
 val constr_out : Dyn.t -> constr
 
-(*i*)
-(* Internal of Pretyping...
- * Unused outside, but useful for debugging
- *)
-val pretype : 
-  type_constraint -> env -> evar_defs ref -> 
-  var_map * (identifier * identifier option) list ->
-  rawconstr -> unsafe_judgment
-
-val pretype_type : 
-  val_constraint -> env -> evar_defs ref ->
-    var_map * (identifier * identifier option) list ->
-    rawconstr -> unsafe_type_judgment
-(*i*)
-
-val interp_sort : rawsort -> sorts
-
+val interp_sort : rawsort -> sorts  
 val interp_elimination_sort : rawsort -> sorts_family
+