Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

13 files changed, 132 insertions, 136 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 88243b60..4cf5336d 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -14,7 +14,7 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
 
-(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 
 open Flags
@@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ 
     Coqlib.check_required_library ["Coq";"Program";"Tactics"];
     Tacinterp.add_tacdef false 
-      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
+      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index a59ad6f5..7bfa107b 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *)
+(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Global
 open Pp
@@ -229,7 +229,8 @@ let subtac (loc, command) =
       debug 2 (Himsg.explain_pretype_error env exn);
       raise e
 	
-  | (Stdpp.Exc_located (loc, e')) as e ->
+  | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+     Stdpp.Exc_located (loc, e') as e) ->
       debug 2 (str "Parsing exception: ");
       (match e' with
       | Type_errors.TypeError (env, exn) ->
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index c7182bd2..04bf54d3 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *)
+(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Cases
 open Util
@@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	    t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
 	      tomatchs sign (lift tomatchs_len t)
       in
-      let arity = 
-	it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
+      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 *)
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 15addb44..9a5539e2 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -73,26 +73,18 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
+      let t' = substl subst t in
       let c = interp_casted_constr_evars isevars env ce t' in
+      isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
       let d = na, Some c, t' in
-	(na, c) :: subst, d :: instctx)
+	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
-
 let type_class_instance_params isevars env id n ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
       let t' = replace_vars subst t in
-      let c = 
-(* 	if ce = superclass_ce then *)
-	(* 	  (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
-	(* 	     in instance search. *\) *)
-	(* 	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
-	(* 	else *)
-	interp_casted_constr_evars isevars env ce t' 
-      in
+      let c = interp_casted_constr_evars isevars env ce t' in
       let d = na, Some c, t' in
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
@@ -140,9 +132,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
-    let ctx, c = Classes.decompose_named_assum c' in
+    let ctx, c = Sign.decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -155,11 +147,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	  let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
-  let env' = Classes.push_named_context ctx' env in
+  let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
-  let substctx = Typeclasses.nf_substitution sigma subst in
+  let substctx = List.map (Evarutil.nf_evar sigma) subst in
   let subst, _propsctx = 
     let props = 
       List.map (fun (x, l, d) -> 
@@ -172,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	List.fold_left
 	  (fun (props, rest) (id,_,_) -> 
 	    try 
-	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+	      let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
 		Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		c :: props, rest'
 	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -184,20 +176,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	else
 	  type_ctx_instance isevars env' k.cl_props props substctx
   in
-  let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in
+  let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
     isevars := Evarutil.nf_evar_defs !isevars;
-    let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx')
-    and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') 
+    let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+    and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
     in
       isevars := undefined_evars !isevars;
       Evarutil.check_evars env Evd.empty !isevars termtype;
-(*   let imps =  *)
-(*     Util.list_map_i  *)
-(*       (fun i binder -> *)
-(* 	match binder with *)
-(* 	ExplByPos (i, Some na), (true, true)) *)
-(*       1 ctx *)
-(*   in *)
       let hook gr = 
 	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 	let inst = Typeclasses.new_instance k pri global cst in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 43f00107..afb0d38d 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*)
+(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -26,11 +26,11 @@ open Classes
 
 val type_ctx_instance :     Evd.evar_defs ref ->
     Environ.env ->
-    (Names.identifier * 'a * Term.constr) list ->
+    ('a * Term.constr option * Term.constr) list ->
     Topconstr.constr_expr list ->
-    (Names.identifier * Term.constr) list ->
-    (Names.identifier * Term.constr) list *
-    (Names.identifier * Term.constr option * Term.constr) list
+    Term.constr list ->
+    Term.constr list *
+    ('a * Term.constr option * Term.constr) list
 
 val new_instance : 
   ?global:bool ->
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b45e23d0..b046f0b3 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -111,41 +111,31 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-(*       (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++  *)
-(* 		  str " and "++ my_print_constr env y ++  *)
-(* 		  str " with evars: " ++ spc () ++ *)
-(* 		  my_print_evardefs !isevars); *)
-(*        with _ -> ()); *)
     let rec coerce_unify env x y =
-(*       (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++  *)
-(* 		  str " to "++ my_print_constr env y) *)
-(*        with _ -> ()); *)
       let x = hnf env isevars x and y = hnf env isevars y in
 	try 
 	  isevars := the_conv_x_leq env x y !isevars;
-	  (* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
-	  (* 			str " and "++ my_print_constr env y); *)
-	  (* 	 with _ -> ()); *)
 	  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.decomp_n_prod env (evars_of !isevars) 1 c with
+	| [(na,b,t)], c -> (na,t), c
+	| _ -> raise NoSubtacCoercion
+      in
       let rec coerce_application typ typ' c c' l l' =
 	let len = Array.length l in
 	let rec aux tele typ typ' i co = 
-(* 	  (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
-(* 			 str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	    with _ -> ()); *)
 	  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) = destProd typ in
-		let (n', eqT', restT') = destProd typ' in
+		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) = destProd typ in
-		let (n', eqT', restT') = destProd typ' in
+		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
@@ -163,12 +153,12 @@ module Coercion = struct
 				      [| 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 aux [] typ typ' 0 (fun x -> x)
+	in 
+	  if isEvar c || isEvar c' then
+	    (* Second-order unification needed. *)
+	    raise NoSubtacCoercion;
+	  aux [] typ typ' 0 (fun x -> x)
       in
-(* 	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
-(* 		       str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	  with _ -> ()); *)
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
 	      (match s, s' with
@@ -179,13 +169,6 @@ module Coercion = struct
 	  | Prod (name, a, b), Prod (name', a', b') ->
 	      let name' = Name (Nameops.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 *)
-(* 	      let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *)
-(* 	      let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *)
-(* 	      let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *)
-(* 				     mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *)
-
 	      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 c1 (mkRel 1) in
@@ -295,7 +278,6 @@ module Coercion = struct
     and subset_coerce env isevars x y =
       match disc_subset x with
 	  Some (u, p) -> 
-	    (* trace (str "Inserting projection ");	     *)
 	    let c = coerce_unify env u y in
 	    let f x = 
 	      app_opt c (mkApp ((Lazy.force sig_).proj1, 
@@ -423,7 +405,11 @@ module Coercion = struct
       isevars, { uj_val = app_opt ct j.uj_val; 
 		 uj_type = typ' }
 
-
+  let inh_coerce_to_prod loc env isevars t =
+    let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+    let _, typ' = mu env isevars typ in
+      isevars, (fst t, typ')
+	
   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
@@ -504,14 +490,13 @@ module Coercion = struct
 	  None -> 0, 0
 	| Some (init, cur) -> init, cur
     in
-      (* a little more effort to get products is needed *)
-      try let rels, rng = decompose_prod_n nabs t in
+      try 
+	let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
-	if noccur_with_meta 0 (succ nabsinit) rng then (
-(* 	  trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+	if noccur_with_meta 1 (succ nabs) rng then (
 	  let env', t, t' =
-	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+	    let env' = push_rel_context rels env in
 	      env', rng, lift nabs t'
 	  in
 	    try
@@ -523,6 +508,4 @@ module Coercion = struct
 		error_cannot_coerce env' sigma (t, t'))
 	else isevars
       with _ -> isevars
-(*  	trace (str "decompose_prod_n failed"); *)
-(*  	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
 end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5bff6ad1..a2f54b02 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 
 let push_named_context = List.fold_right push_named
 
+let check_evars env initial_sigma evd c =
+  let sigma = evars_of evd in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (evk,args) ->
+          assert (Evd.mem sigma evk);
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk evd in
+	      (match k with
+	      | QuestionMark _ -> ()
+	      | _ ->
+		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
+		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
+  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed =
   let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
     
   let recdefs = List.length rec_sign in
-(*   List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
-(*   List.iter (check_evars env Evd.empty evd) fixtypes; *)
-(*   check_mutuality env kind (List.combine fixnames fixdefs); *)
+  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+  List.iter (check_evars env Evd.empty evd) fixtypes;
+  Command.check_mutuality env kind (List.combine fixnames fixdefs);
 
   (* Russell-specific code *)
 
   (* Get the interesting evars, those that were not instanciated *)
   let isevars = Evd.undefined_evars evd in
-  trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
   let evm = Evd.evars_of isevars in
-  trace (str "got the evm, recdefs is " ++ int recdefs);
   (* Solve remaining evars *)
   let rec collect_evars id def typ imps = 
-    let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
       (* Generalize by the recursive prototypes  *)
     let def = 
       Termops.it_mkNamedLambda_or_LetIn def rec_sign
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 27520867..3a6a351b 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -42,6 +42,7 @@ val interp_binder :     Evd.evar_defs ref ->
     Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
 
 
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 55cdc7c4..a393e2c9 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" [])
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
@@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac =
 	       true		 
 	    else false
 	  with
+	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	    | Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	    | Refiner.FailError (_, s) ->
 		user_err_loc (obl.obl_location, "solve_obligation", s)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0e987cf2..ad76bdeb 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Global
 open Pp
@@ -117,7 +117,6 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id bl c tycon =
-(*   let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
   let c = Command.abstract_constr_expr c bl in
   let tycon = 
     match tycon with
@@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon =
   let imps = Implicit_quantifiers.implicits_of_rawterm c in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars (evars_of !isevars) in
-    evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps
+  let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+    evm, coqc, ty, imps
 
 open Subtac_obligations
 
 let subtac_proof kind env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
-  let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
-  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
+  let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
+  let evm' = Subtac_utils.evars_of_term evm evm' coqt in
+  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
     add_definition id def ty ~implicits:imps ~kind:kind evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index afa5817f..559b6ac1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Pp
 open Util
@@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) 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)
 	  | RCoFix i -> 
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env isevars fixj tycon
@@ -273,13 +275,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
+	let length = List.length args in 
 	let ftycon = 
-	  match tycon with
-	      None -> None
+	  if length > 0 then
+	    match tycon with
+	    | None -> None
 	    | Some (None, ty) -> mk_abstr_tycon length ty
 	    | Some (Some (init, cur), ty) ->
 		Some (Some (length + init, length + cur), ty)
+	  else tycon
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
@@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
               let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
-		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      Option.iter (fun ty -> isevars :=
+			Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon;
+		      let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in
+		      isevars := evd;
+		      let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
-		      let tycon = 
-			Option.map 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
@@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
@@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RLambda(loc,name,k,c1,c2)      ->
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	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') 
+	  isevars tycon 
+	in
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env isevars lvar c1 in
 	let var = (name,None,j.utj_val) in
 	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-	  judge_of_abstraction env name j j'
+	let resj = judge_of_abstraction env name j j' in
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env isevars lvar c1 in
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 3ceea173..05fc0803 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,5 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import List.
 
 Set Implicit Arguments.
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Section Accessors.
   Variable A : Set.
 
-  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=  
     fun l =>
       match l with
         | nil => !
@@ -39,7 +39,7 @@ Section app.
 
   Next Obligation.
     intros.
-    destruct_call app ; subtac_simpl.
+    destruct_call app ; program_simpl.
   Defined.
   
   Program Lemma app_id_l : forall l : list A, l = nil ++ l.
@@ -49,7 +49,7 @@ Section app.
   
   Program Lemma app_id_r : forall l : list A, l = l ++ nil.
   Proof.
-    induction l ; simpl ; auto.
+    induction l ; simpl in * ; auto. 
     rewrite <- IHl ; auto.
   Qed.
 
@@ -70,16 +70,24 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    intros.
-    inversion H.
+    simpl in *. auto with arith. 
   Defined.
 
+  Next Obligation.
+  Proof.
+    inversion H.
+  Qed.
+
   Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
     match l, n with
       | hd :: _, 0 => hd
       | _ :: tl, S n' => nth' tl n'
       | nil, _ => !
     end.
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith. 
+  Defined.
 
   Next Obligation.
   Proof.
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 87ab47d6..2e17959c 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,9 +1,12 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import JMeq.
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Program.
 
 Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
 
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
@@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct
   end.
 
 Require Import Omega.
-
+Solve All Obligations.
 Next Obligation.
-  intros.
-  simpl in l0.
-  apply le_S_n ; exact l0.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct_call take ; subtac_simpl.
+  destruct_call take ; program_simpl.
 Defined.
 
 Next Obligation.
   intros.
-  inversion l0.
+  inversion H.
 Defined.