Second step of integration of Program:

- Remove useless functorization of Pretyping
- Move Program coercion/cases code inside pretyping/, enabled according
to a flag.

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

8 files changed, 1587 insertions, 938 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 2883df6d7a..8652dbd036 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -362,9 +362,6 @@ let evd_comb2 f evdref x y =
   evdref := evd';
   y
 
-
-module Cases_F(Coercion : Coercion.S) : S = struct
-
 let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) =
   (* Ideally, we could find a common inductive type to which both the
      term to match and the patterns coerce *)
@@ -1642,7 +1639,8 @@ let build_initial_predicate arsign pred =
     | _ -> assert false
   in buildrec 0 pred [] (List.rev arsign)
 
-let extract_arity_signature env0 tomatchl tmsign =
+let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
+  let lift = if dolift then lift else fun n t -> t in
   let get_one_sign n tm (na,t) =
     match tm with
       | NotInd (bo,typ) ->
@@ -1652,7 +1650,7 @@ let extract_arity_signature env0 tomatchl tmsign =
  	    user_err_loc (loc,"",
 	    str"Unexpected type annotation for a term of non inductive type."))
       | IsInd (term,IndType(indf,realargs),_) ->
-          let indf' = lift_inductive_family n indf in
+          let indf' = if dolift then lift_inductive_family n indf else indf in
 	  let (ind,_) = dest_ind_family indf' in
 	  let nparams_ctxt,nrealargs_ctxt = inductive_nargs_env env0 ind in
 	  let arsign = fst (get_arity env0 indf') in
@@ -1786,11 +1784,511 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
       sigma,nal,pred)
     preds
 
+module ProgramCases = struct
+
+open Program
+
+let ($) f x = f x
+
+let string_of_name name =
+  match name with
+    | Anonymous -> "anonymous"
+    | Name n -> string_of_id n
+
+let id_of_name n = id_of_string (string_of_name n)
+
+let make_prime_id name =
+  let str = string_of_name name in
+    id_of_string str, id_of_string (str ^ "'")
+
+let prime avoid name =
+  let previd, id = make_prime_id name in
+    previd, next_ident_away id avoid
+
+let make_prime avoid prevname =
+  let previd, id = prime !avoid prevname in
+    avoid := id :: !avoid;
+    previd, id
+
+let eq_id avoid id =
+  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid' = next_ident_away hid avoid in
+    hid'
+
+let mk_eq typ x y = mkApp (delayed_force coq_eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (delayed_force coq_eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y =
+  mkApp (delayed_force coq_JMeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (delayed_force coq_JMeq_refl, [| typ; x |])
+
+let hole = GHole (dummy_loc, Evd.QuestionMark (Evd.Define true))
+
+let constr_of_pat env isevars arsign pat avoid =
+  let rec typ env (ty, realargs) pat avoid =
+    match pat with
+    | PatVar (l,name) ->
+	let name, avoid = match name with
+	    Name n -> name, avoid
+	  | Anonymous ->
+	      let previd, id = prime avoid (Name (id_of_string "wildcard")) in
+		Name id, id :: avoid
+	in
+	  PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid
+    | PatCstr (l,((_, i) as cstr),args,alias) ->
+	let cind = inductive_of_constructor cstr in
+	let IndType (indf, _) = 
+	  try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty)
+	  with Not_found -> error_case_not_inductive env 
+	    {uj_val = ty; uj_type = Typing.type_of env !isevars ty}
+	in
+	let ind, params = dest_ind_family indf in
+	if ind <> cind then error_bad_constructor_loc l cstr ind;
+	let cstrs = get_constructors env indf in
+	let ci = cstrs.(i-1) in
+	let nb_args_constr = ci.cs_nargs in
+	assert(nb_args_constr = List.length args);
+	let patargs, args, sign, env, n, m, avoid =
+	  List.fold_right2
+	    (fun (na, c, t) ua (patargs, args, sign, env, n, m, avoid)  ->
+	       let pat', sign', arg', typ', argtypargs, n', avoid =
+		 typ env (substl args (liftn (List.length sign) (succ (List.length args)) t), []) ua avoid
+	       in
+	       let args' = arg' :: List.map (lift n') args in
+	       let env' = push_rels sign' env in
+		 (pat' :: patargs, args', sign' @ sign, env', n' + n, succ m, avoid))
+	    ci.cs_args (List.rev args) ([], [], [], env, 0, 0, avoid)
+	in
+	let args = List.rev args in
+	let patargs = List.rev patargs in
+	let pat' = PatCstr (l, cstr, patargs, alias) in
+	let cstr = mkConstruct ci.cs_cstr in
+	let app = applistc cstr (List.map (lift (List.length sign)) params) in
+	let app = applistc app args in
+	let apptype = Retyping.get_type_of env ( !isevars) app in
+	let IndType (indf, realargs) = find_rectype env ( !isevars) apptype in
+	  match alias with
+	      Anonymous ->
+		pat', sign, app, apptype, realargs, n, avoid
+	    | Name id ->
+		let sign = (alias, None, lift m ty) :: sign in
+		let avoid = id :: avoid in
+		let sign, i, avoid =
+		  try
+		    let env = push_rels sign env in
+		    isevars := the_conv_x_leq (push_rels sign env) (lift (succ m) ty) (lift 1 apptype) !isevars;
+		    let eq_t = mk_eq (lift (succ m) ty)
+		      (mkRel 1) (* alias *)
+		      (lift 1 app) (* aliased term *)
+		    in
+		    let neq = eq_id avoid id in
+		      (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid
+		  with Reduction.NotConvertible -> sign, 1, avoid
+		in
+		  (* Mark the equality as a hole *)
+		  pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
+  in
+  let pat', sign, patc, patty, args, z, avoid = typ env (pi3 (List.hd arsign), List.tl arsign) pat avoid in
+    pat', (sign, patc, (pi3 (List.hd arsign), args), pat'), avoid
+
+
+(* shadows functional version *)
+let eq_id avoid id =
+  let hid = id_of_string ("Heq_" ^ string_of_id id) in
+  let hid' = next_ident_away hid !avoid in
+    avoid := hid' :: !avoid;
+    hid'
+
+let rels_of_patsign =
+  List.map (fun ((na, b, t) as x) ->
+    match b with
+      | Some t' when kind_of_term t' = Rel 0 -> (na, None, t)
+      | _ -> x)
+
+let vars_of_ctx ctx =
+  let _, y =
+    List.fold_right (fun (na, b, t)  (prev, vars) ->
+      match b with
+	| Some t' when kind_of_term t' = Rel 0 ->
+	    prev,
+	    (GApp (dummy_loc,
+		(GRef (dummy_loc, delayed_force coq_eq_refl_ref)), 
+		   [hole; GVar (dummy_loc, prev)])) :: vars
+	| _ ->
+	    match na with
+		Anonymous -> raise (Invalid_argument "vars_of_ctx")
+	      | Name n -> n, GVar (dummy_loc, n) :: vars)
+      ctx (id_of_string "vars_of_ctx_error", [])
+  in List.rev y
+
+let rec is_included x y =
+  match x, y with
+    | PatVar _, _ -> true
+    | _, PatVar _ -> true
+    | PatCstr (l, (_, i), args, alias), PatCstr (l', (_, i'), args', alias')  ->
+	if i = i' then List.for_all2 is_included args args'
+	else false
+
+(* liftsign is the current pattern's complete signature length. Hence pats is already typed in its
+   full signature. However prevpatterns are in the original one signature per pattern form.
+ *)
+let build_ineqs prevpatterns pats liftsign =
+  let _tomatchs = List.length pats in
+  let diffs =
+    List.fold_left
+      (fun c eqnpats ->
+	  let acc = List.fold_left2
+	    (* ppat is the pattern we are discriminating against, curpat is the current one. *)
+	    (fun acc (ppat_sign, ppat_c, (ppat_ty, ppat_tyargs), ppat)
+	      (curpat_sign, curpat_c, (curpat_ty, curpat_tyargs), curpat) ->
+	      match acc with
+		  None -> None
+		| Some (sign, len, n, c) -> (* FixMe: do not work with ppat_args *)
+		    if is_included curpat ppat then
+		      (* Length of previous pattern's signature *)
+		      let lens = List.length ppat_sign in
+		      (* Accumulated length of previous pattern's signatures *)
+		      let len' = lens + len in
+		      let acc =
+			((* Jump over previous prevpat signs *)
+			  lift_rel_context len ppat_sign @ sign,
+			  len',
+			  succ n, (* nth pattern *)
+			  mkApp (delayed_force coq_eq_ind,
+				[| lift (len' + liftsign) curpat_ty;
+				   liftn (len + liftsign) (succ lens) ppat_c ;
+				   lift len' curpat_c |]) ::
+			    List.map (lift lens (* Jump over this prevpat signature *)) c)
+		      in Some acc
+		    else None)
+	   (Some ([], 0, 0, [])) eqnpats pats
+	 in match acc with
+	     None -> c
+	   | Some (sign, len, _, c') ->
+	       let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_conj c'))
+		 (lift_rel_context liftsign sign)
+	       in
+		 conj :: c)
+      [] prevpatterns
+  in match diffs with [] -> None
+    | _ -> Some (mk_coq_conj diffs)
+
+let subst_rel_context k ctx subst =
+  let (_, ctx') =
+    List.fold_right
+      (fun (n, b, t) (k, acc) ->
+	 (succ k, (n, Option.map (substnl subst k) b, substnl subst k t) :: acc))
+      ctx (k, [])
+  in ctx'
+
+let lift_rel_contextn n k sign =
+  let rec liftrec k = function
+    | (na,c,t)::sign ->
+	(na,Option.map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
+    | [] -> []
+  in
+  liftrec (rel_context_length sign + k) sign
+
+let constrs_of_pats typing_fun env isevars eqns tomatchs sign neqs arity =
+  let i = ref 0 in
+  let (x, y, z) =
+    List.fold_left
+      (fun (branches, eqns, prevpatterns) eqn ->
+	 let _, newpatterns, pats =
+	   List.fold_left2
+	     (fun (idents, newpatterns, pats) pat arsign ->
+		let pat', cpat, idents = constr_of_pat env isevars arsign pat idents in
+		  (idents, pat' :: newpatterns, cpat :: pats))
+	      ([], [], []) eqn.patterns sign
+	 in
+	 let newpatterns = List.rev newpatterns and opats = List.rev pats in
+	 let rhs_rels, pats, signlen =
+	   List.fold_left
+	     (fun (renv, pats, n) (sign,c, (s, args), p) ->
+	       (* Recombine signatures and terms of all of the row's patterns *)
+	       let sign' = lift_rel_context n sign in
+	       let len = List.length sign' in
+		 (sign' @ renv,
+		 (* lift to get outside of previous pattern's signatures. *)
+		 (sign', liftn n (succ len) c, (s, List.map (liftn n (succ len)) args), p) :: pats,
+		 len + n))
+	     ([], [], 0) opats in
+	 let pats, _ = List.fold_left
+	   (* lift to get outside of past patterns to get terms in the combined environment. *)
+	   (fun (pats, n) (sign, c, (s, args), p) ->
+	     let len = List.length sign in
+	       ((rels_of_patsign sign, lift n c, (s, List.map (lift n) args), p) :: pats, len + n))
+	   ([], 0) pats
+	 in
+	 let ineqs = build_ineqs prevpatterns pats signlen in
+	 let rhs_rels' = rels_of_patsign rhs_rels in
+	 let _signenv = push_rel_context rhs_rels' env in
+	 let arity =
+	   let args, nargs =
+	     List.fold_right (fun (sign, c, (_, args), _) (allargs,n) ->
+	       (args @ c :: allargs, List.length args + succ n))
+	       pats ([], 0)
+	   in
+	   let args = List.rev args in
+	     substl args (liftn signlen (succ nargs) arity)
+	 in
+	 let rhs_rels', tycon =
+	   let neqs_rels, arity =
+	     match ineqs with
+	     | None -> [], arity
+	     | Some ineqs ->
+		 [Anonymous, None, ineqs], lift 1 arity
+	   in
+	   let eqs_rels, arity = decompose_prod_n_assum neqs arity in
+	     eqs_rels @ neqs_rels @ rhs_rels', arity
+	 in
+	 let rhs_env = push_rels rhs_rels' env in
+	 let j = typing_fun (mk_tycon tycon) rhs_env eqn.rhs.it in
+	 let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels'
+	 and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in
+	 let branch_name = id_of_string ("program_branch_" ^ (string_of_int !i)) in
+	 let branch_decl = (Name branch_name, Some (lift !i bbody), (lift !i btype)) in
+	 let branch =
+	   let bref = GVar (dummy_loc, branch_name) in
+	     match vars_of_ctx rhs_rels with
+		 [] -> bref
+	       | l -> GApp (dummy_loc, bref, l)
+	 in
+	 let branch = match ineqs with
+	     Some _ -> GApp (dummy_loc, branch, [ hole ])
+	   | None -> branch
+	 in
+	 incr i;
+	 let rhs = { eqn.rhs with it = Some branch } in
+	   (branch_decl :: branches,
+	   { eqn with patterns = newpatterns; rhs = rhs } :: eqns,
+	   opats :: prevpatterns))
+      ([], [], []) eqns
+  in x, y
+
+(* Builds the predicate. If the predicate is dependent, its context is
+ * made of 1+nrealargs assumptions for each matched term in an inductive
+ * type and 1 assumption for each term not _syntactically_ in an
+ * inductive type.
+
+ * Each matched terms are independently considered dependent or not.
+
+ * A type constraint but no annotation case: it is assumed non dependent.
+ *)
+
+let lift_ctx n ctx =
+  let ctx', _ =
+    List.fold_right (fun (c, t) (ctx, n') -> (liftn n n' c, liftn_tomatch_type n n' t) :: ctx, succ n') ctx ([], 0)
+  in ctx'
+
+(* Turn matched terms into variables. *)
+let abstract_tomatch env tomatchs tycon =
+  let prev, ctx, names, tycon =
+    List.fold_left
+      (fun (prev, ctx, names, tycon) (c, t) ->
+	 let lenctx =  List.length ctx in
+	 match kind_of_term c with
+	     Rel n -> (lift lenctx c, lift_tomatch_type lenctx t) :: prev, ctx, names, tycon
+	   | _ ->
+	       let tycon = Option.map
+		 (fun t -> subst_term (lift 1 c) (lift 1 t)) tycon in
+	       let name = next_ident_away (id_of_string "filtered_var") names in
+		 (mkRel 1, lift_tomatch_type (succ lenctx) t) :: lift_ctx 1 prev,
+	       (Name name, Some (lift lenctx c), lift lenctx $ type_of_tomatch t) :: ctx,
+	       name :: names, tycon)
+      ([], [], [], tycon) tomatchs
+  in List.rev prev, ctx, tycon
+
+let is_dependent_ind = function
+    IsInd (_, IndType (indf, args), _) when List.length args > 0 -> true
+  | _ -> false
+
+let build_dependent_signature env evars avoid tomatchs arsign =
+  let avoid = ref avoid in
+  let arsign = List.rev arsign in
+  let allnames = List.rev (List.map (List.map pi1) arsign) in
+  let nar = List.fold_left (fun n names -> List.length names + n) 0 allnames in
+  let eqs, neqs, refls, slift, arsign' =
+    List.fold_left2
+      (fun (eqs, neqs, refl_args, slift, arsigns) (tm, ty) arsign ->
+	 (* The accumulator:
+	    previous eqs,
+	    number of previous eqs,
+	    lift to get outside eqs and in the introduced variables ('as' and 'in'),
+	    new arity signatures
+	 *)
+	 match ty with
+	     IsInd (ty, IndType (indf, args), _) when List.length args > 0 ->
+	       (* Build the arity signature following the names in matched terms as much as possible *)
+	       let argsign = List.tl arsign in (* arguments in inverse application order *)
+	       let (appn, appb, appt) as _appsign = List.hd arsign in (* The matched argument *)
+	       let argsign = List.rev argsign in (* arguments in application order *)
+	       let env', nargeqs, argeqs, refl_args, slift, argsign' =
+		 List.fold_left2
+		   (fun (env, nargeqs, argeqs, refl_args, slift, argsign') arg (name, b, t) ->
+		      let argt = Retyping.get_type_of env evars arg in
+		      let eq, refl_arg =
+			if Reductionops.is_conv env evars argt t then
+			  (mk_eq (lift (nargeqs + slift) argt)
+			     (mkRel (nargeqs + slift))
+			     (lift (nargeqs + nar) arg),
+			   mk_eq_refl argt arg)
+			else
+			  (mk_JMeq (lift (nargeqs + slift) t)
+			     (mkRel (nargeqs + slift))
+			     (lift (nargeqs + nar) argt)
+			     (lift (nargeqs + nar) arg),
+			   mk_JMeq_refl argt arg)
+		      in
+		      let previd, id =
+			let name =
+			  match kind_of_term arg with
+			      Rel n -> pi1 (lookup_rel n env)
+			    | _ -> name
+			in
+			  make_prime avoid name
+		      in
+			(env, succ nargeqs,
+			 (Name (eq_id avoid previd), None, eq) :: argeqs,
+			 refl_arg :: refl_args,
+			 pred slift,
+			 (Name id, b, t) :: argsign'))
+		   (env, neqs, [], [], slift, []) args argsign
+	       in
+	       let eq = mk_JMeq
+		 (lift (nargeqs + slift) appt)
+		 (mkRel (nargeqs + slift))
+		 (lift (nargeqs + nar) ty)
+		 (lift (nargeqs + nar) tm)
+	       in
+	       let refl_eq = mk_JMeq_refl ty tm in
+	       let previd, id = make_prime avoid appn in
+		 (((Name (eq_id avoid previd), None, eq) :: argeqs) :: eqs,
+		 succ nargeqs,
+		 refl_eq :: refl_args,
+		 pred slift,
+		 (((Name id, appb, appt) :: argsign') :: arsigns))
+
+	   | _ ->
+	       (* Non dependent inductive or not inductive, just use a regular equality *)
+	       let (name, b, typ) = match arsign with [x] -> x | _ -> assert(false) in
+	       let previd, id = make_prime avoid name in
+	       let arsign' = (Name id, b, typ) in
+	       let tomatch_ty = type_of_tomatch ty in
+	       let eq =
+		 mk_eq (lift nar tomatch_ty)
+		   (mkRel slift) (lift nar tm)
+	       in
+		 ([(Name (eq_id avoid previd), None, eq)] :: eqs, succ neqs,
+		  (mk_eq_refl tomatch_ty tm) :: refl_args,
+		  pred slift, (arsign' :: []) :: arsigns))
+      ([], 0, [], nar, []) tomatchs arsign
+  in
+  let arsign'' = List.rev arsign' in
+    assert(slift = 0); (* we must have folded over all elements of the arity signature *)
+    arsign'', allnames, nar, eqs, neqs, refls
+
+let context_of_arsign l =
+  let (x, _) = List.fold_right
+    (fun c (x, n) ->
+      (lift_rel_context n c @ x, List.length c + n))
+    l ([], 0)
+  in x
+
+let compile_program_cases loc style (typing_function, evdref) tycon env (predopt, tomatchl, eqns) =
+  let typing_fun tycon env = function
+    | Some t ->	typing_function tycon env evdref t
+    | None -> coq_unit_judge () in
+
+  (* We build the matrix of patterns and right-hand side *)
+  let matx = matx_of_eqns env eqns in
+
+  (* We build the vector of terms to match consistently with the *)
+  (* constructors found in patterns *)
+  let tomatchs = coerce_to_indtype typing_function evdref env matx tomatchl in
+  let tycon = valcon_of_tycon tycon in
+  let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env tomatchs tycon in
+  let env = push_rel_context tomatchs_lets env in
+  let len = List.length eqns in
+  let sign, allnames, signlen, eqs, neqs, args =
+    (* The arity signature *)
+    let arsign = extract_arity_signature ~dolift:false env tomatchs tomatchl in
+      (* Build the dependent arity signature, the equalities which makes
+	 the first part of the predicate and their instantiations. *)
+    let avoid = [] in
+      build_dependent_signature env ( !evdref) avoid tomatchs arsign
+
+  in
+  let tycon, arity =
+    match tycon' with
+    | None -> let ev = mkExistential env evdref in ev, ev
+    | Some t ->
+	let pred = 
+	  try
+	    let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in
+	      (* The tycon may be ill-typed after abstraction. *)
+	    let env' = push_rel_context (context_of_arsign sign) env in
+	      ignore(Typing.sort_of env' !evdref pred); pred
+	  with _ -> 
+	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
+	      lift nar t
+	in Option.get tycon, pred
+  in
+  let neqs, arity =
+    let ctx = context_of_arsign eqs in
+    let neqs = List.length ctx in
+      neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
+  in
+  let lets, matx =
+    (* Type the rhs under the assumption of equations *)
+    constrs_of_pats typing_fun env evdref matx tomatchs sign neqs arity
+  in
+  let matx = List.rev matx in
+  let _ = assert(len = List.length lets) in
+  let env = push_rels lets env in
+  let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in
+  let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in
+  let args = List.rev_map (lift len) args in
+  let pred = liftn len (succ signlen) arity in
+  let nal, pred = build_initial_predicate sign pred 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,[],Anonymous)) tomatchs in
+
+  let typing_function tycon env evdref = function
+    | Some t ->	typing_function tycon env evdref t
+    | None -> coq_unit_judge () in
+
+  let pb =
+    { env      = env;
+      evdref  = evdref;
+      pred     = pred;
+      tomatch  = initial_pushed;
+      history  = start_history (List.length initial_pushed);
+      mat      = matx;
+      caseloc  = loc;
+      casestyle= style;
+      typing_function = typing_function } in
+
+  let j = compile pb in
+    (* We check for unused patterns *)
+    List.iter (check_unused_pattern env) matx;
+    let body = it_mkLambda_or_LetIn (applistc j.uj_val args) lets in
+    let j =
+      { uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
+	uj_type = nf_evar !evdref tycon; }
+    in j
+end
+
 (**************************************************************************)
 (* Main entry of the matching compilation                                 *)
 
 let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, eqns) =
-
+  if predopt = None && Flags.is_program_mode () then
+    ProgramCases.compile_program_cases loc style (typing_fun, evdref) 
+      tycon env (predopt, tomatchl, eqns)
+  else
+      
   (* We build the matrix of patterns and right-hand side *)
   let matx = matx_of_eqns env eqns in
 
@@ -1798,6 +2296,8 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
   (* constructors found in patterns *)
   let tomatchs = coerce_to_indtype typing_fun evdref env matx tomatchl in
 
+
+
   (* If an elimination predicate is provided, we check it is compatible
      with the type of arguments to match; if none is provided, we
      build alternative possible predicates *)
@@ -1861,4 +2361,3 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
   (* We coerce to the tycon (if an elim predicate was provided) *)
   inh_conv_coerce_to_tycon loc env evdref j tycon
 
-end
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index fcfee055c4..39677f38b9 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -48,13 +48,10 @@ val error_needs_inversion : env -> constr -> types -> 'a
 
 (** {6 Compilation primitive. } *)
 
-module type S = sig
-  val compile_cases :
-    loc -> case_style ->
-    (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
-    type_constraint ->
-    env -> glob_constr option * tomatch_tuples * cases_clauses ->
-    unsafe_judgment
-end
-
-module Cases_F(C : Coercion.S) : S
+val compile_cases :
+  loc -> case_style ->
+  (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
+  type_constraint ->
+  env -> glob_constr option * tomatch_tuples * cases_clauses ->
+  unsafe_judgment
+
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index eb014af464..2b93a5fca8 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -31,219 +31,456 @@ open Retyping
 open Evd
 open Termops
 
-module type S = sig
-  (*s Coercions. *)
-
-  (* [inh_app_fun env evd 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_map -> unsafe_judgment -> evar_map * unsafe_judgment
-
-  (* [inh_coerce_to_sort env evd 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_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
-
-  (* [inh_coerce_to_base env evd j] coerces [j] to its base type; i.e. it
-     inserts a coercion into [j], if needed, in such a way it gets as
-     type its base type (the notion depends on the coercion system) *)
-  val inh_coerce_to_base : loc ->
-    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
-
-  (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *)
-  val inh_coerce_to_prod : loc ->
-    env -> evar_map -> types -> evar_map * types
-
-  (* [inh_conv_coerce_to loc env evd 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_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
-
-  val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
-
-  (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
-     is coercible to an object of type [t'] adding evar constraints if needed;
-     it fails if no coercion exists *)
-  val inh_conv_coerces_to : loc ->
-    env -> evar_map -> types -> types -> evar_map
-
-  (* [inh_pattern_coerce_to loc env evd 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  -> Glob_term.cases_pattern -> inductive -> inductive -> Glob_term.cases_pattern
-end
-
-module Default = struct
-  (* Typing operations dealing with coercions *)
-  exception NoCoercion
-
-  (* 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"
+(* Typing operations dealing with coercions *)
+exception NoCoercion
+
+(* 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 Glob_term.PatVar (loc, Anonymous) else pat in
+	 Glob_term.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 p = lookup_pattern_path_between (ind1,ind2) in
+    apply_pattern_coercion loc pat p
+
+(* Program coercions *)
+
+open Program
+
+let make_existential loc ?(opaque = Define true) env isevars c =
+  Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c
+
+let app_opt env evars f t =
+  whd_betaiota !evars (app_opt f t)
+
+let pair_of_array a = (a.(0), a.(1))
+let make_name s = Name (id_of_string s)
+
+let rec disc_subset x =
+  match kind_of_term x with
+  | App (c, l) ->
+      (match kind_of_term c with
+       Ind i ->
+	 let len = Array.length l in
+	 let sigty = delayed_force sig_typ in
+	   if len = 2 && i = Term.destInd sigty
+	   then
+	     let (a, b) = pair_of_array l in
+	       Some (a, b)
+	   else None
+       | _ -> None)
+  | _ -> None
+
+exception NoSubtacCoercion
+  
+let hnf env isevars c = whd_betadeltaiota env isevars c
+let hnf_nodelta env evars c = whd_betaiota evars c
+
+let lift_args n sign =
+  let rec liftrec k = function
+    | t::sign -> liftn n k t :: (liftrec (k-1) sign)
+    | [] -> []
+  in
+    liftrec (List.length sign) sign
+
+let rec mu env isevars t =
+  let rec aux v =
+    let v = hnf env !isevars v in
+      match disc_subset v with
+      Some (u, p) ->
+	let f, ct = aux u in
+	let p = hnf env !isevars p in
+	  (Some (fun x ->
+		   app_opt env isevars 
+		     f (mkApp (delayed_force sig_proj1,
+			       [| u; p; x |]))),
+	   ct)
+      | None -> (None, v)
+  in aux t
+
+and coerce loc env isevars (x : Term.constr) (y : Term.constr)
+    : (Term.constr -> Term.constr) option
+    =
+  let rec coerce_unify env x y =
+    let x = hnf env !isevars x and y = hnf env !isevars y in
+      try
+	isevars := the_conv_x_leq env x y !isevars;
+	None
+      with Reduction.NotConvertible -> coerce' env x y
+  and coerce' env x y : (Term.constr -> Term.constr) option =
+    let subco () = subset_coerce env isevars x y in
+    let dest_prod c =
+      match Reductionops.splay_prod_n env ( !isevars) 1 c with
+      | [(na,b,t)], c -> (na,t), c
+      | _ -> raise NoSubtacCoercion
     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 Glob_term.PatVar (loc, Anonymous) else pat in
-	   Glob_term.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 p = lookup_pattern_path_between (ind1,ind2) in
-      apply_pattern_coercion loc pat p
-
-  let saturate_evd env evd =
-    Typeclasses.resolve_typeclasses
-      ~onlyargs:true ~split:true ~fail:false env evd
-
-  (* appliquer le chemin de coercions p à hj *)
-  let apply_coercion env sigma 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 env sigma 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 evd j =
-    let t = whd_betadeltaiota env evd j.uj_type in
-      match kind_of_term t with
-	| Prod (_,_,_) -> (evd,j)
-	| Evar ev ->
-	    let (evd',t) = define_evar_as_product evd ev in
-	      (evd',{ uj_val = j.uj_val; uj_type = t })
-	| _ ->
-      	    let t,p =
-	      lookup_path_to_fun_from env evd j.uj_type in
-	      (evd,apply_coercion env evd p j t)
-
-  let inh_app_fun env evd j =
-    try inh_app_fun env evd j
-    with Not_found ->
-      try inh_app_fun env (saturate_evd env evd) j
-      with Not_found -> (evd, j)
-
-  let inh_tosort_force loc env evd j =
-    try
-      let t,p = lookup_path_to_sort_from env evd j.uj_type in
-      let j1 = apply_coercion env evd p j t in
-      let j2 = on_judgment_type (whd_evar evd) j1 in
-        (evd,type_judgment env j2)
-    with Not_found ->
-      error_not_a_type_loc loc env evd j
-
-  let inh_coerce_to_sort loc env evd j =
-    let typ = whd_betadeltaiota env evd j.uj_type in
-      match kind_of_term typ with
-	| Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
-	| Evar ev when not (is_defined_evar evd ev) ->
-	    let (evd',s) = define_evar_as_sort evd ev in
-	      (evd',{ utj_val = j.uj_val; utj_type = s })
-	| _ ->
-	    inh_tosort_force loc env evd j
-
-  let inh_coerce_to_base loc env evd j = (evd, j)
-  let inh_coerce_to_prod loc env evd t = (evd, t)
-
-  let inh_coerce_to_fail env evd rigidonly v t c1 =
-    if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
-    then
-      raise NoCoercion
-    else
+    let rec coerce_application typ typ' c c' l l' =
+      let len = Array.length l in
+      let rec aux tele typ typ' i co =
+	if i < len then
+	  let hdx = l.(i) and hdy = l'.(i) in
+	    try isevars := the_conv_x_leq env hdx hdy !isevars;
+	      let (n, eqT), restT = dest_prod typ in
+	      let (n', eqT'), restT' = dest_prod typ' in
+		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
+	    with Reduction.NotConvertible ->
+	      let (n, eqT), restT = dest_prod typ in
+	      let (n', eqT'), restT' = dest_prod typ' in
+	      let _ =
+		try isevars := the_conv_x_leq env eqT eqT' !isevars
+		with Reduction.NotConvertible -> raise NoSubtacCoercion
+	      in
+		(* Disallow equalities on arities *)
+		if Reduction.is_arity env eqT then raise NoSubtacCoercion;
+		let restargs = lift_args 1
+		  (List.rev (Array.to_list (Array.sub l (succ i) (len - (succ i)))))
+		in
+		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
+		let pred = mkLambda (n, eqT, applistc (lift 1 c) args) in
+		let eq = mkApp (delayed_force coq_eq_ind, [| eqT; hdx; hdy |]) in
+		let evar = make_existential loc env isevars eq in
+		let eq_app x = mkApp (delayed_force coq_eq_rect,
+				      [| eqT; hdx; pred; x; hdy; evar|]) in
+		  aux (hdy :: tele) (subst1 hdx restT) 
+		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
+	else Some co
+      in
+	if isEvar c || isEvar c' then
+	  (* Second-order unification needed. *)
+	  raise NoSubtacCoercion;
+	aux [] typ typ' 0 (fun x -> x)
+    in
+      match (kind_of_term x, kind_of_term y) with
+      | Sort s, Sort s' ->
+	  (match s, s' with
+	   Prop x, Prop y when x = y -> None
+	   | Prop _, Type _ -> None
+	   | Type x, Type y when x = y -> None (* false *)
+	   | _ -> subco ())
+      | Prod (name, a, b), Prod (name', a', b') ->
+	  let name' = Name (Namegen.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
+	  let env' = push_rel (name', None, a') env in
+	  let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
+	    (* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
+	  let coec1 = app_opt env' isevars c1 (mkRel 1) in
+	    (* env, x : a' |- c1[x] : lift 1 a *)
+	  let c2 = coerce_unify env' (subst1 coec1 (liftn 1 2 b)) b' in
+	    (* env, x : a' |- c2 : b[c1[x]/x]] > b' *)
+	    (match c1, c2 with
+	     | None, None -> None
+	     | _, _ ->
+		 Some
+		   (fun f ->
+		      mkLambda (name', a',
+				app_opt env' isevars c2
+				  (mkApp (Term.lift 1 f, [| coec1 |])))))
+
+      | App (c, l), App (c', l') ->
+	  (match kind_of_term c, kind_of_term c' with
+	   Ind i, Ind i' -> (* Inductive types *)
+	     let len = Array.length l in
+	     let sigT = delayed_force sigT_typ in
+	     let prod = delayed_force prod_typ in
+	       (* Sigma types *)
+	       if len = Array.length l' && len = 2 && i = i'
+		 && (i = Term.destInd sigT || i = Term.destInd prod)
+	       then
+		 if i = Term.destInd sigT
+		 then
+		   begin
+		     let (a, pb), (a', pb') =
+		       pair_of_array l, pair_of_array l'
+		     in
+		     let c1 = coerce_unify env a a' in
+		     let rec remove_head a c =
+		       match kind_of_term c with
+		       | Lambda (n, t, t') -> c, t'
+			   (*| Prod (n, t, t') -> t'*)
+		       | Evar (k, args) ->
+			   let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in
+			     isevars := evs;
+			     let (n, dom, rng) = destLambda t in
+			     let (domk, args) = destEvar dom in
+			       isevars := define domk a !isevars;
+			       t, rng
+		       | _ -> raise NoSubtacCoercion
+		     in
+		     let (pb, b), (pb', b') = remove_head a pb, remove_head a' pb' in
+		     let env' = push_rel (make_name "x", None, a) env in
+		     let c2 = coerce_unify env' b b' in
+		       match c1, c2 with
+		       None, None ->
+			 None
+		       | _, _ ->
+			   Some
+			     (fun x ->
+				let x, y =
+				  app_opt env' isevars c1 (mkApp (delayed_force sigT_proj1,
+								  [| a; pb; x |])),
+				  app_opt env' isevars c2 (mkApp (delayed_force sigT_proj2,
+								  [| a; pb; x |]))
+				in
+				  mkApp (delayed_force sigT_intro, [| a'; pb'; x ; y |]))
+		   end
+		 else
+		   begin
+		     let (a, b), (a', b') =
+		       pair_of_array l, pair_of_array l'
+		     in
+		     let c1 = coerce_unify env a a' in
+		     let c2 = coerce_unify env b b' in
+		       match c1, c2 with
+		       None, None -> None
+		       | _, _ ->
+			   Some
+			     (fun x ->
+				let x, y =
+				  app_opt env isevars c1 (mkApp (delayed_force prod_proj1,
+								 [| a; b; x |])),
+				  app_opt env isevars c2 (mkApp (delayed_force prod_proj2,
+								 [| a; b; x |]))
+				in
+				  mkApp (delayed_force prod_intro, [| a'; b'; x ; y |]))
+		   end
+	       else
+		 if i = i' && len = Array.length l' then
+		   let evm =  !isevars in
+		     (try subco ()
+		      with NoSubtacCoercion ->
+			let typ = Typing.type_of env evm c in
+			let typ' = Typing.type_of env evm c' in
+			  (* 			     if not (is_arity env evm typ) then *)
+			  coerce_application typ typ' c c' l l')
+		       (* 			     else subco () *)
+		 else
+		   subco ()
+	   | x, y when x = y ->
+	       if Array.length l = Array.length l' then
+		 let evm =  !isevars in
+		 let lam_type = Typing.type_of env evm c in
+		 let lam_type' = Typing.type_of env evm c' in
+		   (* 			 if not (is_arity env evm lam_type) then ( *)
+		   coerce_application lam_type lam_type' c c' l l'
+		     (* 			 ) else subco () *)
+	       else subco ()
+	   | _ -> subco ())
+      | _, _ ->  subco ()
+
+  and subset_coerce env isevars x y =
+    match disc_subset x with
+    Some (u, p) ->
+      let c = coerce_unify env u y in
+      let f x =
+	app_opt env isevars c (mkApp (delayed_force sig_proj1,
+				      [| u; p; x |]))
+      in Some f
+    | None ->
+	match disc_subset y with
+	Some (u, p) ->
+	  let c = coerce_unify env x u in
+	    Some
+	      (fun x ->
+		 let cx = app_opt env isevars c x in
+		 let evar = make_existential loc env isevars (mkApp (p, [| cx |]))
+		 in
+		   (mkApp
+		      (delayed_force sig_intro,
+		       [| u; p; cx; evar |])))
+	| None ->
+	    raise NoSubtacCoercion
+	      (*isevars := Evd.add_conv_pb (Reduction.CONV, x, y) !isevars;
+		None*)
+  in coerce_unify env x y
+
+let coerce_itf loc env isevars v t c1 =
+  let evars = ref isevars in
+  let coercion = coerce loc env evars t c1 in
+  let t = Option.map (app_opt env evars coercion) v in
+    !evars, t
+
+
+
+let saturate_evd env evd =
+  Typeclasses.resolve_typeclasses
+    ~onlyargs:true ~split:true ~fail:false env evd
+
+(* appliquer le chemin de coercions p à hj *)
+let apply_coercion env sigma 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 env sigma 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 evd j =
+  let t = whd_betadeltaiota env evd j.uj_type in
+    match kind_of_term t with
+    | Prod (_,_,_) -> (evd,j)
+    | Evar ev ->
+	let (evd',t) = define_evar_as_product evd ev in
+	  (evd',{ uj_val = j.uj_val; uj_type = t })
+    | _ ->
+      	try let t,p =
+	  lookup_path_to_fun_from env evd j.uj_type in
+	  (evd,apply_coercion env evd p j t)
+	with Not_found when Flags.is_program_mode () ->
+	  try
+	    let isevars = ref evd in
+	    let coercef, t = mu env isevars t in
+	    let res = { uj_val = app_opt env isevars coercef j.uj_val; uj_type = t } in
+	      (!isevars, res)
+	  with NoSubtacCoercion | NoCoercion ->
+	    (evd,j)
+
+let inh_app_fun env evd j =
+  try inh_app_fun env evd j
+  with Not_found ->
+    try inh_app_fun env (saturate_evd env evd) j
+    with Not_found -> (evd, j)
+
+let inh_tosort_force loc env evd j =
+  try
+    let t,p = lookup_path_to_sort_from env evd j.uj_type in
+    let j1 = apply_coercion env evd p j t in
+    let j2 = on_judgment_type (whd_evar evd) j1 in
+      (evd,type_judgment env j2)
+  with Not_found ->
+    error_not_a_type_loc loc env evd j
+
+let inh_coerce_to_sort loc env evd j =
+  let typ = whd_betadeltaiota env evd j.uj_type in
+    match kind_of_term typ with
+    | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
+    | Evar ev when not (is_defined_evar evd ev) ->
+	let (evd',s) = define_evar_as_sort evd ev in
+	  (evd',{ utj_val = j.uj_val; utj_type = s })
+    | _ ->
+	inh_tosort_force loc env evd j
+
+let inh_coerce_to_base loc env evd j =
+  if Flags.is_program_mode () then
+    let isevars = ref evd in
+    let typ = hnf env !isevars j.uj_type in
+    let ct, typ' = mu env isevars typ in
+    let res =
+      { uj_val = app_opt env isevars ct j.uj_val;
+	uj_type = typ' }
+    in !isevars, res
+  else (evd, j)
+
+let inh_coerce_to_prod loc env evd t =
+  if Flags.is_program_mode () then
+    let isevars = ref evd in
+    let typ = hnf env !isevars t in
+    let _, typ' = mu env isevars typ in
+      !isevars, typ'
+  else (evd, t)
+
+let inh_coerce_to_fail env evd rigidonly v t c1 =
+  if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
+  then
+    raise NoCoercion
+  else
     let v', t' =
       try
 	let t2,t1,p = lookup_path_between env evd (t,c1) in
 	  match v with
-	      Some v ->
-		let j =
-		  apply_coercion env evd p
-		    {uj_val = v; uj_type = t} t2 in
-		  Some j.uj_val, j.uj_type
-	    | None -> None, t
+	  Some v ->
+	    let j =
+	      apply_coercion env evd p
+		{uj_val = v; uj_type = t} t2 in
+	      Some j.uj_val, j.uj_type
+	  | None -> None, t
       with Not_found -> raise NoCoercion
     in
       try (the_conv_x_leq env t' c1 evd, v')
       with Reduction.NotConvertible -> raise NoCoercion
 
-  let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
-    try (the_conv_x_leq env t c1 evd, v)
-    with Reduction.NotConvertible ->
+let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
+  try (the_conv_x_leq env t c1 evd, v)
+  with Reduction.NotConvertible ->
     try inh_coerce_to_fail env evd rigidonly v t c1
     with NoCoercion ->
-    match
+      match
       kind_of_term (whd_betadeltaiota env evd t),
       kind_of_term (whd_betadeltaiota env evd c1)
-    with
-    | Prod (name,t1,t2), Prod (_,u1,u2) ->
-        (* Conversion did not work, we may succeed with a coercion. *)
-        (* We eta-expand (hence possibly modifying the original term!) *)
-	(* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
-	(* has type forall (x:u1), u2 (with v' recursively obtained) *)
-        (* Note: we retype the term because sort-polymorphism may have *)
-        (* weaken its type *)
-	let name = match name with
-	  | Anonymous -> Name (id_of_string "x")
-	  | _ -> name in
-	let env1 = push_rel (name,None,u1) env in
-	let (evd', v1) =
-	  inh_conv_coerce_to_fail loc env1 evd rigidonly
-            (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
-        let v1 = Option.get v1 in
-	let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
-	let t2 = match v2 with
-	  | None -> subst_term v1 t2
-	  | Some v2 -> Retyping.get_type_of env1 evd' v2 in
-	let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
-	(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
-    | _ -> raise NoCoercion
-
-  (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
-  let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
-    let (evd', val') =
-      try
-	inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-      with NoCoercion ->
-	let evd = saturate_evd env evd in
-	  try
-	    inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
-	  with NoCoercion ->
-	    error_actual_type_loc loc env evd cj t
-    in
-    let val' = match val' with Some v -> v | None -> assert(false) in
-      (evd',{ uj_val = val'; uj_type = t })
-
-  let inh_conv_coerce_to = inh_conv_coerce_to_gen false
-  let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+      with
+      | Prod (name,t1,t2), Prod (_,u1,u2) ->
+          (* Conversion did not work, we may succeed with a coercion. *)
+          (* We eta-expand (hence possibly modifying the original term!) *)
+	  (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *)
+	  (* has type forall (x:u1), u2 (with v' recursively obtained) *)
+          (* Note: we retype the term because sort-polymorphism may have *)
+          (* weaken its type *)
+	  let name = match name with
+	    | Anonymous -> Name (id_of_string "x")
+	    | _ -> name in
+	  let env1 = push_rel (name,None,u1) env in
+	  let (evd', v1) =
+	    inh_conv_coerce_to_fail loc env1 evd rigidonly
+              (Some (mkRel 1)) (lift 1 u1) (lift 1 t1) in
+          let v1 = Option.get v1 in
+	  let v2 = Option.map (fun v -> beta_applist (lift 1 v,[v1])) v in
+	  let t2 = match v2 with
+	    | None -> subst_term v1 t2
+	    | Some v2 -> Retyping.get_type_of env1 evd' v2 in
+	  let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
+	    (evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
+      | _ -> raise NoCoercion
 
-  let inh_conv_coerces_to loc env evd t t' =
+(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
+let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
+  let (evd', val') =
     try
-      fst (inh_conv_coerce_to_fail loc env evd true None t t')
+      inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
     with NoCoercion ->
-      evd (* Maybe not enough information to unify *)
-    
-end
+      let evd = saturate_evd env evd in
+	try
+	  inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
+	with NoCoercion ->
+	  (if Flags.is_program_mode () then
+	     try
+	       coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
+	     with NoSubtacCoercion ->
+	       error_actual_type_loc loc env evd cj t
+	   else error_actual_type_loc loc env evd cj t)
+  in
+  let val' = match val' with Some v -> v | None -> assert(false) in
+    (evd',{ uj_val = val'; uj_type = t })
+
+let inh_conv_coerce_to = inh_conv_coerce_to_gen false
+let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true
+
+let inh_conv_coerces_to loc env evd t t' =
+  try
+    fst (inh_conv_coerce_to_fail loc env evd true None t t')
+  with NoCoercion ->
+    evd (* Maybe not enough information to unify *)
+      
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 91cb693abf..45566e9fbc 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -16,51 +16,47 @@ open Environ
 open Evarutil
 open Glob_term
 
-module type S = sig
-  (** {6 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_map -> unsafe_judgment -> evar_map * 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_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
-
-  (** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
-     inserts a coercion into [j], if needed, in such a way it gets as
-     type its base type (the notion depends on the coercion system) *)
-  val inh_coerce_to_base : loc ->
-    env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
-
-  (** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
-  val inh_coerce_to_prod : loc ->
-    env -> evar_map -> types -> evar_map * types
-
-  (** [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_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
-
-  val inh_conv_coerce_rigid_to : loc ->
-    env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
-
-  (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
-     is coercible to an object of type [t'] adding evar constraints if needed;
-     it fails if no coercion exists *)
-  val inh_conv_coerces_to : loc ->
-    env -> evar_map -> types -> types -> evar_map
-
-  (** [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
-
-module Default : S
+(** {6 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_map -> unsafe_judgment -> evar_map * 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_map -> unsafe_judgment -> evar_map * unsafe_type_judgment
+
+(** [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it
+    inserts a coercion into [j], if needed, in such a way it gets as
+    type its base type (the notion depends on the coercion system) *)
+val inh_coerce_to_base : loc ->
+  env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment
+
+(** [inh_coerce_to_prod env isevars t] coerces [t] to a product type *)
+val inh_coerce_to_prod : loc ->
+  env -> evar_map -> types -> evar_map * types
+
+(** [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_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+
+val inh_conv_coerce_rigid_to : loc ->
+  env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment
+
+(** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t]
+    is coercible to an object of type [t'] adding evar constraints if needed;
+    it fails if no coercion exists *)
+val inh_conv_coerces_to : loc ->
+  env -> evar_map -> types -> types -> evar_map
+
+(** [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
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4f286efe7a..e75dfcca85 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -105,8 +105,10 @@ let interp_elimination_sort = function
 
 let resolve_evars env evdref fail_evar resolve_classes =
   if resolve_classes then
-    evdref := (Typeclasses.resolve_typeclasses ~onlyargs:false
-		 ~split:true ~fail:fail_evar env !evdref);
+    (evdref := Typeclasses.resolve_typeclasses ~onlyargs:true
+       ~split:true ~fail:true env !evdref;
+     evdref := Typeclasses.resolve_typeclasses ~onlyargs:false
+       ~split:true ~fail:fail_evar env !evdref);
   (* Resolve eagerly, potentially making wrong choices *)
   evdref := (try consider_remaining_unif_problems
 	       ~ts:(Typeclasses.classes_transparent_state ()) env !evdref
@@ -136,277 +138,198 @@ let solve_remaining_evars fail_evar use_classes hook env initial_sigma (evd,c) =
   (* Side-effect *)
   !evdref,c
 
-module type S =
-sig
-
-  module Cases : Cases.S
-
-  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
-  val allow_anonymous_refs : bool ref
-
-  (* Generic call to the interpreter from glob_constr 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 : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
-
-  val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
-
-  (* More general entry point with evars from ltac *)
-
-  (* Generic call to the interpreter from glob_constr to constr, failing
-     unresolved holes in the glob_constr cannot be instantiated.
-
-     In [understand_ltac expand_evars sigma env ltac_env constraint c],
-
-     expand_evars : expand inferred evars by their value if any
-     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 :
-    bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> glob_constr -> pure_open_constr
-
-  (* Standard call to get a constr from a glob_constr, resolving implicit args *)
-
-  val understand : evar_map -> env -> ?expected_type:Term.types ->
-    glob_constr -> constr
-
-  (* Idem but the glob_constr is intended to be a type *)
-
-  val understand_type : evar_map -> env -> glob_constr -> constr
-
-  (* A generalization of the two previous case *)
-
-  val understand_gen : typing_constraint -> evar_map -> env ->
-    glob_constr -> constr
-
-  (* Idem but returns the judgment of the understood term *)
-
-  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
-
-  (* Idem but do not fail on unresolved evars *)
-
-  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
-
-  (*i*)
-  (* Internal of Pretyping...
-   * Unused outside, but useful for debugging
-   *)
-  val pretype :
-    type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> glob_constr -> unsafe_judgment
-
-  val pretype_type :
-    val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> glob_constr -> unsafe_type_judgment
-
-  val pretype_gen :
-    bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> glob_constr -> constr
-
-    (*i*)
-end
-
-module Pretyping_F (Coercion : Coercion.S) = struct
-
-  module Cases = Cases.Cases_F(Coercion)
-
-  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
-  let allow_anonymous_refs = ref false
-
-  let program_mode = ref false
-
-  let evd_comb0 f evdref =
-    let (evd',x) = f !evdref in
-      evdref := evd';
-      x
-
-  let evd_comb1 f evdref x =
-    let (evd',y) = f !evdref x in
-      evdref := evd';
-      y
-
-  let evd_comb2 f evdref x y =
-    let (evd',z) = f !evdref x y in
-      evdref := evd';
-      z
-
-  let evd_comb3 f evdref x y z =
-    let (evd',t) = f !evdref x y z in
-      evdref := evd';
-      t
-
-  let mt_evd = Evd.empty
-
-  (* 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 evdref 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 evdref (vdefj.(i)).uj_type
-		    (lift lt lar.(i))) then
-            error_ill_typed_rec_body_loc loc env !evdref
-              i lna vdefj lar
-	done
-
-  (* coerce to tycon if any *)
-  let inh_conv_coerce_to_tycon loc env evdref j = function
-    | None -> j
-    | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
-
-  (* used to enforce a name in Lambda when the type constraints itself
-     is named, hence possibly dependent *)
-
-  let orelse_name name name' = match name with
-    | Anonymous -> name'
-    | _ -> name
-
-  let invert_ltac_bound_name env id0 id =
-    try mkRel (pi1 (lookup_rel_id id (rel_context env)))
-    with Not_found ->
-      errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
-	str " depends on pattern variable name " ++ pr_id id ++
-	str " which is not bound in current context.")
-
-  let protected_get_type_of env sigma c =
-    try Retyping.get_type_of env sigma c
-    with Anomaly _ ->
-      errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
-
-  let pretype_id loc env sigma (lvar,unbndltacvars) id =
-    (* Look for the binder of [id] *)
-    try
-      let (n,_,typ) = lookup_rel_id id (rel_context env) in
+(* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+let allow_anonymous_refs = ref false
+
+let evd_comb0 f evdref =
+  let (evd',x) = f !evdref in
+    evdref := evd';
+    x
+
+let evd_comb1 f evdref x =
+  let (evd',y) = f !evdref x in
+    evdref := evd';
+    y
+
+let evd_comb2 f evdref x y =
+  let (evd',z) = f !evdref x y in
+    evdref := evd';
+    z
+
+let evd_comb3 f evdref x y z =
+  let (evd',t) = f !evdref x y z in
+    evdref := evd';
+    t
+
+let mt_evd = Evd.empty
+
+(* 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 evdref 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 evdref (vdefj.(i)).uj_type
+		  (lift lt lar.(i))) then
+          error_ill_typed_rec_body_loc loc env !evdref
+            i lna vdefj lar
+      done
+
+(* coerce to tycon if any *)
+let inh_conv_coerce_to_tycon loc env evdref j = function
+  | None -> j
+  | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t
+
+let push_rels vars env = List.fold_right push_rel vars env
+
+(* used to enforce a name in Lambda when the type constraints itself
+   is named, hence possibly dependent *)
+
+let orelse_name name name' = match name with
+  | Anonymous -> name'
+  | _ -> name
+
+let invert_ltac_bound_name env id0 id =
+  try mkRel (pi1 (lookup_rel_id id (rel_context env)))
+  with Not_found ->
+    errorlabstrm "" (str "Ltac variable " ++ pr_id id0 ++
+		       str " depends on pattern variable name " ++ pr_id id ++
+		       str " which is not bound in current context.")
+
+let protected_get_type_of env sigma c =
+  try Retyping.get_type_of env sigma c
+  with Anomaly _ ->
+    errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
+
+let pretype_id loc env sigma (lvar,unbndltacvars) id =
+  (* Look for the binder of [id] *)
+  try
+    let (n,_,typ) = lookup_rel_id id (rel_context env) in
+>>>>>>> Second step of integration of Program:
       { uj_val  = mkRel n; uj_type = lift n typ }
-    with Not_found ->
+  with Not_found ->
     (* Check if [id] is an ltac variable *)
     try
       let (ids,c) = List.assoc id lvar in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
-      { uj_val = c; uj_type = protected_get_type_of env sigma c }
-    with Not_found ->
-    (* Check if [id] is a section or goal variable *)
-    try
-      let (_,_,typ) = lookup_named id env in
-      { uj_val  = mkVar id; uj_type = typ }
-    with Not_found ->
-    (* [id] not found, build nice error message if [id] yet known from ltac *)
-    try
-      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
+	{ uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
-    (* [id] not found, standard error message *)
-      error_var_not_found_loc loc id
-
-  let evar_kind_of_term sigma c =
-    kind_of_term (whd_evar sigma c)
-
-  (*************************************************************************)
-  (* Main pretyping function                                               *)
-
-  let pretype_ref evdref env ref =
-    let c = constr_of_global ref in
-      make_judge c (Retyping.get_type_of env Evd.empty c)
-
-  let pretype_sort evdref = function
-    | GProp c -> judge_of_prop_contents c
-    | GType _ -> evd_comb0 judge_of_new_Type evdref
-
-  exception Found of fixpoint
-
-  let new_type_evar evdref env loc =
-    evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
-
-  (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
-  (* in environment [env], with existential variables [evdref] and *)
-  (* the type constraint tycon *)
-  let rec pretype (tycon : type_constraint) env evdref lvar = function
-    | GRef (loc,ref) ->
-	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_ref evdref env ref)
-	  tycon
-
-    | GVar (loc, id) ->
-	inh_conv_coerce_to_tycon loc env evdref
-	  (pretype_id loc env !evdref lvar id)
-	  tycon
-
-    | GEvar (loc, evk, 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_filtered_context (Evd.find !evdref evk) in
-	let args = match instopt with
-          | None -> instance_from_named_context hyps
-          | Some inst -> failwith "Evar subtitutions not implemented" in
-	let c = mkEvar (evk, args) in
-	let j = (Retyping.get_judgment_of env !evdref c) in
-	  inh_conv_coerce_to_tycon loc env evdref j tycon
-
-    | GPatVar (loc,(someta,n)) ->
-	let ty =
-          match tycon with
-            | Some ty -> ty
-            | None -> new_type_evar evdref env loc in
-        let k = MatchingVar (someta,n) in
+      (* Check if [id] is a section or goal variable *)
+      try
+	let (_,_,typ) = lookup_named id env in
+	  { uj_val  = mkVar id; uj_type = typ }
+      with Not_found ->
+	(* [id] not found, build nice error message if [id] yet known from ltac *)
+	try
+	  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 ->
+	  (* [id] not found, standard error message *)
+	  error_var_not_found_loc loc id
+
+let evar_kind_of_term sigma c =
+  kind_of_term (whd_evar sigma c)
+
+(*************************************************************************)
+(* Main pretyping function                                               *)
+
+let pretype_ref evdref env ref =
+  let c = constr_of_global ref in
+    make_judge c (Retyping.get_type_of env Evd.empty c)
+
+let pretype_sort evdref = function
+  | GProp c -> judge_of_prop_contents c
+  | GType _ -> evd_comb0 judge_of_new_Type evdref
+
+exception Found of fixpoint
+
+let new_type_evar evdref env loc =
+  evd_comb0 (fun evd -> Evarutil.new_type_evar evd env ~src:(loc,InternalHole)) evdref
+
+(* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *)
+(* in environment [env], with existential variables [evdref] and *)
+(* the type constraint tycon *)
+let rec pretype (tycon : type_constraint) env evdref lvar = function
+  | GRef (loc,ref) ->
+      inh_conv_coerce_to_tycon loc env evdref
+	(pretype_ref evdref env ref)
+	tycon
+
+  | GVar (loc, id) ->
+      inh_conv_coerce_to_tycon loc env evdref
+	(pretype_id loc env !evdref lvar id)
+	tycon
+
+  | GEvar (loc, evk, 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_filtered_context (Evd.find !evdref evk) in
+      let args = match instopt with
+        | None -> instance_from_named_context hyps
+        | Some inst -> failwith "Evar subtitutions not implemented" in
+      let c = mkEvar (evk, args) in
+      let j = (Retyping.get_judgment_of env !evdref c) in
+	inh_conv_coerce_to_tycon loc env evdref j tycon
+
+  | GPatVar (loc,(someta,n)) ->
+      let ty =
+        match tycon with
+        | Some ty -> ty
+        | None -> new_type_evar evdref env loc in
+      let k = MatchingVar (someta,n) in
+	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
+
+  | GHole (loc,k) ->
+      let ty =
+        match tycon with
+        | Some ty -> ty
+        | None ->
+	    new_type_evar evdref env loc in
 	{ uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
 
-    | GHole (loc,k) ->
-	let ty =
-          match tycon with
-            | Some ty -> ty
-            | None ->
-		new_type_evar evdref env loc in
-	  { uj_val = e_new_evar evdref env ~src:(loc,k) ty; uj_type = ty }
-
-    | GRec (loc,fixkind,names,bl,lar,vdef) ->
-	let rec type_bl env ctxt = function
-            [] -> ctxt
-          | (na,bk,None,ty)::bl ->
-              let ty' = pretype_type empty_valcon env evdref lvar ty in
-              let dcl = (na,None,ty'.utj_val) in
-		type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
-          | (na,bk,Some bd,ty)::bl ->
-              let ty' = pretype_type empty_valcon env evdref lvar ty in
-              let bd' = pretype (mk_tycon ty'.utj_val) env evdref 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) evdref 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 evdref 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
+  | GRec (loc,fixkind,names,bl,lar,vdef) ->
+      let rec type_bl env ctxt = function
+        [] -> ctxt
+        | (na,bk,None,ty)::bl ->
+            let ty' = pretype_type empty_valcon env evdref lvar ty in
+            let dcl = (na,None,ty'.utj_val) in
+	      type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        | (na,bk,Some bd,ty)::bl ->
+            let ty' = pretype_type empty_valcon env evdref lvar ty in
+            let bd' = pretype (mk_tycon ty'.utj_val) env evdref 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) evdref 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 evdref 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 evdref names ftys vdefj;
 	let ftys = Array.map (nf_evar !evdref) ftys in
 	let fdefs = Array.map (fun x -> nf_evar !evdref (j_val x)) vdefj in
@@ -419,389 +342,395 @@ module Pretyping_F (Coercion : Coercion.S) = struct
                  doesn't seem worth the effort (except for huge mutual
 		 fixpoints ?) *)
 	      let possible_indexes = Array.to_list (Array.mapi
-		(fun i (n,_) -> match n with
-		   | Some n -> [n]
-		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
-		vn)
+						      (fun i (n,_) -> match n with
+						       | Some n -> [n]
+						       | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
+						      vn)
 	      in
 	      let fixdecls = (names,ftys,fdefs) in
 	      let indexes = search_guard loc env possible_indexes fixdecls in
-	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
+		make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | GCoFix i ->
 	      let cofix = (i,(names,ftys,fdefs)) in
-	      (try check_cofix env cofix with e -> Loc.raise loc e);
-	      make_judge (mkCoFix cofix) ftys.(i) in
-	inh_conv_coerce_to_tycon loc env evdref fixj tycon
-
-    | GSort (loc,s) ->
-	let j = pretype_sort evdref s in
-	  inh_conv_coerce_to_tycon loc env evdref j tycon
-
-    | GApp (loc,f,args) ->
-	let fj = pretype empty_tycon env evdref lvar f in
- 	let floc = loc_of_glob_constr f in
-	let length = List.length args in
-	let candargs =
-	  (* Bidirectional typechecking hint: 
-	     parameters of a constructor are completely determined
-	     by a typing constraint *)
-	  if !program_mode && length > 0 && isConstruct fj.uj_val then
-	    match tycon with
-	    | None -> []
-	    | Some ty ->
-	  	let (ind, i) = destConstruct fj.uj_val in
-	  	let npars = inductive_nparams ind in
-	  	  if npars = 0 then []
-	  	  else
-	  	    try
-	  	      (* Does not treat partially applied constructors. *)
-	  	      let IndType (indf, args) = find_rectype env !evdref ty in
-	  	      let (ind',pars) = dest_ind_family indf in
-	  		if ind = ind' then pars
-	  		else (* Let the usual code throw an error *) []
-	  	    with Not_found -> []
- 	  else []
-	in
-	let rec apply_rec env n resj candargs = function
-	  | [] -> resj
-	  | c::rest ->
-	      let argloc = loc_of_glob_constr c in
-	      let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
-              let resty = whd_betadeltaiota env !evdref resj.uj_type in
-      		match kind_of_term resty with
-		| Prod (na,c1,c2) ->
-		    let hj = pretype (mk_tycon c1) env evdref lvar c in
-		    let candargs, ujval =
-		      match candargs with
-		      | [] -> [], j_val hj
-		      | arg :: args -> 
-			  if e_conv env evdref (j_val hj) arg then
-			    args, nf_evar !evdref (j_val hj)
-			  else [], j_val hj
-		    in
-		    let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
-		      apply_rec env (n+1)
-			{ uj_val = value;
-			  uj_type = typ }
-			candargs rest
-
-		  | _ ->
-		      let hj = pretype empty_tycon env evdref lvar c in
-			error_cant_apply_not_functional_loc
-			  (join_loc floc argloc) env !evdref
-	      		  resj [hj]
-	in
-	let resj = apply_rec env 1 fj candargs args in
-	let resj =
-	  match evar_kind_of_term !evdref resj.uj_val with
-	  | App (f,args) ->
-              let f = whd_evar !evdref f in
+		(try check_cofix env cofix with e -> Loc.raise loc e);
+		make_judge (mkCoFix cofix) ftys.(i) in
+	  inh_conv_coerce_to_tycon loc env evdref fixj tycon
+
+  | GSort (loc,s) ->
+      let j = pretype_sort evdref s in
+	inh_conv_coerce_to_tycon loc env evdref j tycon
+
+  | GApp (loc,f,args) ->
+      let fj = pretype empty_tycon env evdref lvar f in
+      let floc = loc_of_glob_constr f in
+      let length = List.length args in
+      let candargs =
+	(* Bidirectional typechecking hint: 
+	   parameters of a constructor are completely determined
+	   by a typing constraint *)
+	if Flags.is_program_mode () && length > 0 && isConstruct fj.uj_val then
+	  match tycon with
+	  | None -> []
+	  | Some ty ->
+	      let (ind, i) = destConstruct fj.uj_val in
+	      let npars = inductive_nparams ind in
+	  	if npars = 0 then []
+	  	else
+	  	  try
+	  	    (* Does not treat partially applied constructors. *)
+	  	    let IndType (indf, args) = find_rectype env !evdref ty in
+	  	    let (ind',pars) = dest_ind_family indf in
+	  	      if ind = ind' then pars
+	  	      else (* Let the usual code throw an error *) []
+	  	  with Not_found -> []
+ 	else []
+      in
+      let rec apply_rec env n resj candargs = function
+	| [] -> resj
+	| c::rest ->
+	    let argloc = loc_of_glob_constr c in
+	    let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in
+            let resty = whd_betadeltaiota env !evdref resj.uj_type in
+      	      match kind_of_term resty with
+	      | Prod (na,c1,c2) ->
+		  let hj = pretype (mk_tycon c1) env evdref lvar c in
+		  let candargs, ujval =
+		    match candargs with
+		    | [] -> [], j_val hj
+		    | arg :: args -> 
+			if e_conv env evdref (j_val hj) arg then
+			  args, nf_evar !evdref (j_val hj)
+			else [], j_val hj
+		  in
+		  let value, typ = applist (j_val resj, [ujval]), subst1 ujval c2 in
+		    apply_rec env (n+1)
+		      { uj_val = value;
+			uj_type = typ }
+		      candargs rest
+
+	      | _ ->
+		  let hj = pretype empty_tycon env evdref lvar c in
+		    error_cant_apply_not_functional_loc
+		      (join_loc floc argloc) env !evdref
+	      	      resj [hj]
+      in
+      let resj = apply_rec env 1 fj candargs args in
+      let resj =
+	match evar_kind_of_term !evdref resj.uj_val with
+	| App (f,args) ->
+            let f = whd_evar !evdref f in
               begin match kind_of_term f with
               | Ind _ | Const _
-		  when isInd f or has_polymorphic_type (destConst f)
-		    ->
+		    when isInd f or has_polymorphic_type (destConst f)
+		      ->
 	          let sigma =  !evdref in
 		  let c = mkApp (f,Array.map (whd_evar sigma) args) in
 	          let t = Retyping.get_type_of env sigma c in
-		  make_judge c (* use this for keeping evars: resj.uj_val *) t
+		    make_judge c (* use this for keeping evars: resj.uj_val *) t
               | _ -> resj end
-	  | _ -> resj in
+	| _ -> resj in
 	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-    | GLambda(loc,name,bk,c1,c2)      ->
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon in
-	let dom_valcon = valcon_of_tycon dom in
-	let j = pretype_type dom_valcon env evdref lvar c1 in
-	let var = (name,None,j.utj_val) in
-	let j' = pretype rng (push_rel var env) evdref lvar c2 in
-	  judge_of_abstraction env (orelse_name name name') j j'
-
-    | GProd(loc,name,bk,c1,c2)        ->
-	let j = pretype_type empty_valcon env evdref lvar c1 in
-	let j' =
-	  if name = Anonymous then
-	    let j = pretype_type empty_valcon env evdref lvar c2 in
-	      { j with utj_val = lift 1 j.utj_val }
-	  else
-	    let var = (name,j.utj_val) in
-	    let env' = push_rel_assum var env in
-	      pretype_type empty_valcon env' evdref lvar c2
-	in
-	let resj =
-	  try judge_of_product env name j j'
-	  with TypeError _ as e -> Loc.raise loc e in
-	  inh_conv_coerce_to_tycon loc env evdref resj tycon
-
-    | GLetIn(loc,name,c1,c2)      ->
-	let j =
-	  match c1 with
-	  | GCast (loc, c, CastConv (DEFAULTcast, t)) ->
-	      let tj = pretype_type empty_valcon env evdref lvar t in
-		pretype (mk_tycon tj.utj_val) env evdref lvar c
-	  | _ -> pretype empty_tycon env evdref lvar c1
-	in
-	let t = refresh_universes j.uj_type in
-	let var = (name,Some j.uj_val,t) in
-        let tycon = lift_tycon 1 tycon in
-	let j' = pretype tycon (push_rel var env) evdref lvar c2 in
-	  { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
-	    uj_type = subst1 j.uj_val j'.uj_type }
-
-    | GLetTuple (loc,nal,(na,po),c,d) ->
-	let cj = pretype empty_tycon env evdref lvar c in
-	let (IndType (indf,realargs)) =
-	  try find_rectype env !evdref cj.uj_type
-	  with Not_found ->
-	    let cloc = loc_of_glob_constr c in
-	      error_case_not_inductive_loc cloc env !evdref 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_rel_context fsign env in
-	      (* Make dependencies from arity signature impossible *)
-	    let arsgn =
-	      let arsgn,_ = get_arity env indf in
-		if not !allow_anonymous_refs then
-		  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
-		else 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_rel_context psign env in
-		     let pj = pretype_type empty_valcon env_p evdref lvar p in
-		     let ccl = nf_evar !evdref 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 !evdref lp inst in
-		     let fj = pretype (mk_tycon fty) env_f evdref lvar d in
-		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let v =
-		       let ind,_ = dest_ind_family indf in
-		       let ci = make_case_info env ind LetStyle in
-		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
-		       mkCase (ci, p, cj.uj_val,[|f|]) in
-		     { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
-
-		 | None ->
-		     let tycon = lift_tycon cs.cs_nargs tycon in
-		     let fj = pretype tycon env_f evdref lvar d in
-		     let f = it_mkLambda_or_LetIn fj.uj_val fsign in
-		     let ccl = nf_evar !evdref 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 !evdref
-			   cj.uj_val in
-		     let ccl = refresh_universes ccl in
-		     let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
-		     let v =
-		       let ind,_ = dest_ind_family indf in
-		       let ci = make_case_info env ind LetStyle in
-		       Typing.check_allowed_sort env !evdref ind cj.uj_val p;
-		       mkCase (ci, p, cj.uj_val,[|f|])
-		     in { uj_val = v; uj_type = ccl })
-
-    | GIf (loc,c,(na,po),b1,b2) ->
-	let cj = pretype empty_tycon env evdref lvar c in
-	let (IndType (indf,realargs)) =
-	  try find_rectype env !evdref cj.uj_type
-	  with Not_found ->
-	    let cloc = loc_of_glob_constr c in
-	      error_case_not_inductive_loc cloc env !evdref 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.");
+  | GLambda(loc,name,bk,c1,c2)      ->
+      let tycon' = evd_comb1
+	(fun evd tycon ->
+	   match tycon with
+	   | None -> evd, tycon
+	   | Some ty ->
+	       let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
+		 evd, Some ty')
+	evdref tycon
+      in
+      let (name',dom,rng) = evd_comb1 (split_tycon loc env) evdref tycon' in
+      let dom_valcon = valcon_of_tycon dom in
+      let j = pretype_type dom_valcon env evdref lvar c1 in
+      let var = (name,None,j.utj_val) in
+      let j' = pretype rng (push_rel var env) evdref lvar c2 in
+	judge_of_abstraction env (orelse_name name name') j j'
+
+  | GProd(loc,name,bk,c1,c2)        ->
+      let j = pretype_type empty_valcon env evdref lvar c1 in
+      let j' =
+	if name = Anonymous then
+	  let j = pretype_type empty_valcon env evdref lvar c2 in
+	    { j with utj_val = lift 1 j.utj_val }
+	else
+	  let var = (name,j.utj_val) in
+	  let env' = push_rel_assum var env in
+	    pretype_type empty_valcon env' evdref lvar c2
+      in
+      let resj =
+	try judge_of_product env name j j'
+	with TypeError _ as e -> Loc.raise loc e in
+	inh_conv_coerce_to_tycon loc env evdref resj tycon
 
+  | GLetIn(loc,name,c1,c2)      ->
+      let j =
+	match c1 with
+	| GCast (loc, c, CastConv (DEFAULTcast, t)) ->
+	    let tj = pretype_type empty_valcon env evdref lvar t in
+	      pretype (mk_tycon tj.utj_val) env evdref lvar c
+	| _ -> pretype empty_tycon env evdref lvar c1
+      in
+      let t = refresh_universes j.uj_type in
+      let var = (name,Some j.uj_val,t) in
+      let tycon = lift_tycon 1 tycon in
+      let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+	{ uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
+	  uj_type = subst1 j.uj_val j'.uj_type }
+
+  | GLetTuple (loc,nal,(na,po),c,d) ->
+      let cj = pretype empty_tycon env evdref lvar c in
+      let (IndType (indf,realargs)) =
+	try find_rectype env !evdref cj.uj_type
+	with Not_found ->
+	  let cloc = loc_of_glob_constr c in
+	    error_case_not_inductive_loc cloc env !evdref 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 =
 	    let arsgn,_ = get_arity env indf in
 	      if not !allow_anonymous_refs then
-		(* Make dependencies from arity signature impossible *)
 		List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
 	      else 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_rel_context psign env in
-		let pj = pretype_type empty_valcon env_p evdref lvar p in
-		let ccl = nf_evar !evdref pj.utj_val in
-		let pred = it_mkLambda_or_LetIn ccl psign in
-		let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) 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 evdref lvar p in
+		 let ccl = nf_evar !evdref 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 !evdref lp inst in
+		 let fj = pretype (mk_tycon fty) env_f evdref lvar d in
+		 let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		 let v =
+		   let ind,_ = dest_ind_family indf in
+		   let ci = make_case_info env ind LetStyle in
+		     Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		     mkCase (ci, p, cj.uj_val,[|f|]) in
+		   { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl }
+
+	     | None ->
+		 let tycon = lift_tycon cs.cs_nargs tycon in
+		 let fj = pretype tycon env_f evdref lvar d in
+		 let f = it_mkLambda_or_LetIn fj.uj_val fsign in
+		 let ccl = nf_evar !evdref 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 !evdref
+		       cj.uj_val in
+		 let ccl = refresh_universes ccl in
+		 let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in
+		 let v =
+		   let ind,_ = dest_ind_family indf in
+		   let ci = make_case_info env ind LetStyle in
+		     Typing.check_allowed_sort env !evdref ind cj.uj_val p;
+		     mkCase (ci, p, cj.uj_val,[|f|])
+		 in { uj_val = v; uj_type = ccl })
+
+  | GIf (loc,c,(na,po),b1,b2) ->
+      let cj = pretype empty_tycon env evdref lvar c in
+      let (IndType (indf,realargs)) =
+	try find_rectype env !evdref cj.uj_type
+	with Not_found ->
+	  let cloc = loc_of_glob_constr c in
+	    error_case_not_inductive_loc cloc env !evdref 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.");
+
+	let arsgn =
+	  let arsgn,_ = get_arity env indf in
+	    if not !allow_anonymous_refs then
+	      (* Make dependencies from arity signature impossible *)
+	      List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+	    else 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 evdref lvar p in
+	      let ccl = nf_evar !evdref pj.utj_val in
+	      let pred = it_mkLambda_or_LetIn ccl psign in
+	      let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in
 	        pred, typ
-	    | None ->
-		let p = match tycon with
-		  | Some ty -> ty
-		  | None -> new_type_evar evdref env loc
-		in
-		  it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
-	  let pred = nf_evar !evdref pred in
-	  let p = nf_evar !evdref p in
-	  let f cs b =
-	    let n = rel_context_length cs.cs_args in
-	    let pi = lift n pred in (* liftn n 2 pred ? *)
-	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
-	    let csgn =
-	      if not !allow_anonymous_refs then
-		List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
-	      else
-		List.map
-		  (fun (n, b, t) ->
-		     match n with
-                         Name _ -> (n, b, t)
-                       | Anonymous -> (Name (id_of_string "H"), b, t))
+	  | None ->
+	      let p = match tycon with
+		| Some ty -> ty
+		| None -> new_type_evar evdref env loc
+	      in
+		it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
+	let pred = nf_evar !evdref pred in
+	let p = nf_evar !evdref p in
+	let f cs b =
+	  let n = rel_context_length cs.cs_args in
+	  let pi = lift n pred in (* liftn n 2 pred ? *)
+	  let pi = beta_applist (pi, [build_dependent_constructor cs]) in
+	  let csgn =
+	    if not !allow_anonymous_refs then
+	      List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args
+	    else
+	      List.map
+		(fun (n, b, t) ->
+		   match n with
+                   Name _ -> (n, b, t)
+                   | Anonymous -> (Name (id_of_string "H"), b, t))
 		cs.cs_args
-	    in
-	    let env_c = push_rel_context csgn env in
-	    let bj = pretype (mk_tycon pi) env_c evdref 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 v =
-	    let ind,_ = dest_ind_family indf in
-	    let ci = make_case_info env ind IfStyle in
-	    let pred = nf_evar !evdref pred in
+	  in
+	  let env_c = push_rels csgn env in
+	  let bj = pretype (mk_tycon pi) env_c evdref 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 v =
+	  let ind,_ = dest_ind_family indf in
+	  let ci = make_case_info env ind IfStyle in
+	  let pred = nf_evar !evdref pred in
 	    Typing.check_allowed_sort env !evdref ind cj.uj_val pred;
 	    mkCase (ci, pred, cj.uj_val, [|b1;b2|])
-	  in
-	    { uj_val = v; uj_type = p }
-
-    | GCases (loc,sty,po,tml,eqns) ->
-	Cases.compile_cases loc sty
-	  ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
-	  tycon env (* loc *) (po,tml,eqns)
-
-    | GCast (loc,c,k) ->
-	let cj =
-	  match k with
-	      CastCoerce ->
-		let cj = pretype empty_tycon env evdref lvar c in
-		  evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
-	    | CastConv (k,t) ->
-		let tj = pretype_type empty_valcon env evdref lvar t in
- 		let cj = pretype empty_tycon env evdref lvar c in
-		let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-		let cj = match k with
-		  | VMcast ->
-                      if not (occur_existential cty || occur_existential tval) then
-		      begin 
-			try 
-			  ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
-			with Reduction.NotConvertible -> 
-			  error_actual_type_loc loc env !evdref cj tval 
-		      end
-                      else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.")
-		  | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
-		in
-		let v = mkCast (cj.uj_val, k, tval) in
-		  { uj_val = v; uj_type = tval }
-	in inh_conv_coerce_to_tycon loc env evdref cj tycon
-
-  (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-  and pretype_type valcon env evdref lvar = function
-    | GHole loc ->
-	(match valcon with
-	   | Some v ->
-               let s =
-		 let sigma =  !evdref 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 ev when is_Type (existential_type sigma ev) ->
-			 evd_comb1 (define_evar_as_sort) evdref ev
-                     | _ -> anomaly "Found a type constraint which is not a type"
-               in
-		 { utj_val = v;
-		   utj_type = s }
-	   | None ->
-	       let s = evd_comb0 new_sort_variable evdref in
-		 { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
-		   utj_type = s})
-    | c ->
-	let j = pretype empty_tycon env evdref lvar c in
-	let loc = loc_of_glob_constr c in
-	let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
-	  match valcon with
-	    | None -> tj
-	    | Some v ->
-		if e_cumul env evdref v tj.utj_val then tj
-		else
-		  error_unexpected_type_loc
-                    (loc_of_glob_constr c) env !evdref tj.utj_val v
-
-  let pretype_gen expand_evar fail_evar resolve_classes evdref 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
+	in
+	  { uj_val = v; uj_type = p }
+
+  | GCases (loc,sty,po,tml,eqns) ->
+      Cases.compile_cases loc sty
+	((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
+	tycon env (* loc *) (po,tml,eqns)
+
+  | GCast (loc,c,k) ->
+      let cj =
+	match k with
+	CastCoerce ->
+	  let cj = pretype empty_tycon env evdref lvar c in
+	    evd_comb1 (Coercion.inh_coerce_to_base loc env) evdref cj
+	| CastConv (k,t) ->
+	    let tj = pretype_type empty_valcon env evdref lvar t in
+ 	    let cj = pretype empty_tycon env evdref lvar c in
+	    let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
+	    let cj = match k with
+	      | VMcast ->
+                  if not (occur_existential cty || occur_existential tval) then
+		    begin 
+		      try 
+			ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
+		      with Reduction.NotConvertible -> 
+			error_actual_type_loc loc env !evdref cj tval 
+		    end
+                  else user_err_loc (loc,"",str "Cannot check cast with vm: unresolved arguments remain.")
+	      | _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
+	    in
+	    let v = mkCast (cj.uj_val, k, tval) in
+	      { uj_val = v; uj_type = tval }
+      in inh_conv_coerce_to_tycon loc env evdref cj tycon
+
+(* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
+and pretype_type valcon env evdref lvar = function
+  | GHole loc ->
+      (match valcon with
+       | Some v ->
+           let s =
+	     let sigma =  !evdref 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 ev when is_Type (existential_type sigma ev) ->
+		   evd_comb1 (define_evar_as_sort) evdref ev
+               | _ -> anomaly "Found a type constraint which is not a type"
+           in
+	     { utj_val = v;
+	       utj_type = s }
+       | None ->
+	   let s = evd_comb0 new_sort_variable evdref in
+	     { utj_val = e_new_evar evdref env ~src:loc (mkSort s);
+	       utj_type = s})
+  | c ->
+      let j = pretype empty_tycon env evdref lvar c in
+      let loc = loc_of_glob_constr c in
+      let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
+	match valcon with
+	| None -> tj
+	| Some v ->
+	    if e_cumul env evdref v tj.utj_val then tj
+	    else
+	      error_unexpected_type_loc
+                (loc_of_glob_constr c) env !evdref tj.utj_val v
+
+let pretype_gen expand_evar fail_evar resolve_classes evdref 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 evdref lvar c).uj_val
-      | IsType ->
-	  (pretype_type empty_valcon env evdref lvar c).utj_val 
-    in
-      resolve_evars env evdref fail_evar resolve_classes;
-      let c = if expand_evar then nf_evar !evdref c' else c' in
-	if fail_evar then check_evars env Evd.empty !evdref c;
-	c
-
-  (* 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 evdref = ref sigma in
-    let j = pretype empty_tycon env evdref ([],[]) c in
-      resolve_evars env evdref true true;
-      let j = j_nf_evar !evdref j in
-	check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
-	j
-
-  let understand_judgment_tcc evdref env c =
-    let j = pretype empty_tycon env evdref ([],[]) c in
-      resolve_evars env evdref false true;
-      j_nf_evar !evdref 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 expand_evar fail_evar resolve_classes sigma env lvar kind c =
-    let evdref = ref sigma in
-    let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
+    | IsType ->
+	(pretype_type empty_valcon env evdref lvar c).utj_val 
+  in
+    resolve_evars env evdref fail_evar resolve_classes;
+    let c = if expand_evar then nf_evar !evdref c' else c' in
+      if fail_evar then check_evars env Evd.empty !evdref c;
+      c
+
+(* 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 evdref = ref sigma in
+  let j = pretype empty_tycon env evdref ([],[]) c in
+    resolve_evars env evdref true true;
+    let j = j_nf_evar !evdref j in
+      check_evars env sigma !evdref (mkCast(j.uj_val,DEFAULTcast, j.uj_type));
+      j
+
+let understand_judgment_tcc evdref env c =
+  let j = pretype empty_tycon env evdref ([],[]) c in
+    resolve_evars env evdref false true;
+    j_nf_evar !evdref 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 expand_evar fail_evar resolve_classes sigma env lvar kind c =
+  let evdref = ref sigma in
+  let c = pretype_gen expand_evar fail_evar resolve_classes evdref env lvar kind c in
     !evdref, c
 
-  (** Entry points of the high-level type synthesis algorithm *)
-
-  let understand_gen kind sigma env c =
-    snd (ise_pretype_gen true true 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 true true sigma env ([],[]) (OfType exptyp) c)
+let understand_gen kind sigma env c =
+  snd (ise_pretype_gen true true true sigma env ([],[]) kind c)
 
-  let understand_type sigma env c =
-    snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
+let understand sigma env ?expected_type:exptyp c =
+  snd (ise_pretype_gen true true true sigma env ([],[]) (OfType exptyp) c)
 
-  let understand_ltac expand_evar sigma env lvar kind c =
-    ise_pretype_gen expand_evar false false sigma env lvar kind c
+let understand_type sigma env c =
+  snd (ise_pretype_gen true true true sigma env ([],[]) IsType c)
 
-  let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
-    ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
+let understand_ltac expand_evar sigma env lvar kind c =
+  ise_pretype_gen expand_evar false false sigma env lvar kind c
 
-  let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
-    pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
-end
+let understand_tcc ?(resolve_classes=true) sigma env ?expected_type:exptyp c =
+  ise_pretype_gen true false resolve_classes sigma env ([],[]) (OfType exptyp) c
 
-module Default : S = Pretyping_F(Coercion.Default)
+let understand_tcc_evars ?(fail_evar=false) ?(resolve_classes=true) evdref env kind c =
+  pretype_gen true fail_evar resolve_classes evdref env ([],[]) kind c
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index cf47d194e3..34bafdb23c 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -23,7 +23,7 @@ open Evarutil
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
 val search_guard :
-    Pp.loc -> env -> int list list -> rec_declaration -> int array
+  Pp.loc -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types option | IsType
 
@@ -33,82 +33,72 @@ type ltac_var_map = var_map * unbound_ltac_var_map
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 type pure_open_constr = evar_map * constr
 
-module type S =
-sig
+(** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+val allow_anonymous_refs : bool ref
+  
+(** Generic call to the interpreter from glob_constr to open_constr, leaving
+    unresolved holes as evars and returning the typing contexts of
+    these evars. Work as [understand_gen] for the rest. *)
 
-  module Cases : Cases.S
+val understand_tcc : ?resolve_classes:bool ->
+  evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
 
-  (** Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
-  val allow_anonymous_refs : bool ref
+val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
+  evar_map ref -> env -> typing_constraint -> glob_constr -> constr
 
-  (** Generic call to the interpreter from glob_constr to open_constr, leaving
-     unresolved holes as evars and returning the typing contexts of
-     these evars. Work as [understand_gen] for the rest. *)
+(** More general entry point with evars from ltac *)
 
-  val understand_tcc : ?resolve_classes:bool ->
-    evar_map -> env -> ?expected_type:types -> glob_constr -> open_constr
+(** Generic call to the interpreter from glob_constr to constr, failing
+    unresolved holes in the glob_constr cannot be instantiated.
 
-  val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool ->
-    evar_map ref -> env -> typing_constraint -> glob_constr -> constr
+    In [understand_ltac expand_evars sigma env ltac_env constraint c],
 
-  (** More general entry point with evars from ltac *)
+    expand_evars : expand inferred evars by their value if any
+    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
+*)
 
-  (** Generic call to the interpreter from glob_constr to constr, failing
-     unresolved holes in the glob_constr cannot be instantiated.
+val understand_ltac :
+  bool -> evar_map -> env -> ltac_var_map ->
+  typing_constraint -> glob_constr -> pure_open_constr
 
-     In [understand_ltac expand_evars sigma env ltac_env constraint c],
+(** Standard call to get a constr from a glob_constr, resolving implicit args *)
 
-     expand_evars : expand inferred evars by their value if any
-     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 : evar_map -> env -> ?expected_type:Term.types ->
+  glob_constr -> constr
 
-  val understand_ltac :
-    bool -> evar_map -> env -> ltac_var_map ->
-    typing_constraint -> glob_constr -> pure_open_constr
+(** Idem but the glob_constr is intended to be a type *)
 
-  (** Standard call to get a constr from a glob_constr, resolving implicit args *)
+val understand_type : evar_map -> env -> glob_constr -> constr
 
-  val understand : evar_map -> env -> ?expected_type:Term.types ->
-    glob_constr -> constr
+(** A generalization of the two previous case *)
 
-  (** Idem but the glob_constr is intended to be a type *)
+val understand_gen : typing_constraint -> evar_map -> env ->
+  glob_constr -> constr
 
-  val understand_type : evar_map -> env -> glob_constr -> constr
+(** Idem but returns the judgment of the understood term *)
 
-  (** A generalization of the two previous case *)
+val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
 
-  val understand_gen : typing_constraint -> evar_map -> env ->
-    glob_constr -> constr
+(** Idem but do not fail on unresolved evars *)
+val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
 
-  (** Idem but returns the judgment of the understood term *)
+(**/**)
+(** Internal of Pretyping... *)
+val pretype :
+  type_constraint -> env -> evar_map ref ->
+  ltac_var_map -> glob_constr -> unsafe_judgment
 
-  val understand_judgment : evar_map -> env -> glob_constr -> unsafe_judgment
+val pretype_type :
+  val_constraint -> env -> evar_map ref ->
+  ltac_var_map -> glob_constr -> unsafe_type_judgment
 
-  (** Idem but do not fail on unresolved evars *)
-  val understand_judgment_tcc : evar_map ref -> env -> glob_constr -> unsafe_judgment
+val pretype_gen :
+  bool -> bool -> bool -> evar_map ref -> env ->
+  ltac_var_map -> typing_constraint -> glob_constr -> constr
 
-  (**/**)
-  (** Internal of Pretyping... *)
-  val pretype :
-    type_constraint -> env -> evar_map ref ->
-    ltac_var_map -> glob_constr -> unsafe_judgment
-
-  val pretype_type :
-    val_constraint -> env -> evar_map ref ->
-    ltac_var_map -> glob_constr -> unsafe_type_judgment
-
-  val pretype_gen :
-    bool -> bool -> bool -> evar_map ref -> env ->
-    ltac_var_map -> typing_constraint -> glob_constr -> constr
-
-  (**/**)
-
-end
-
-module Pretyping_F (C : Coercion.S) : S
-module Default : S
+(**/**)
 
 (** To embed constr in glob_constr *)
 
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index 9eec941463..199adf6a76 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -20,6 +20,7 @@ Tacred
 Typeclasses_errors
 Typeclasses
 Classops
+Program
 Coercion
 Unification
 Detyping
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index be6d90a264..983b9fd618 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -23,7 +23,7 @@ open Glob_term
 open Evarutil
 open Pretype_errors
 open Retyping
-open Coercion.Default
+open Coercion
 open Recordops
 
 let occur_meta_or_undefined_evar evd c =