Rewrite of Program Fixpoint to overcome the previous limitations:

- The measure can now refer to all the formal arguments
- The recursive calls can make all the arguments vary as well
- Generalized to any relation and measure (new syntax {measure m on R})
This relies on an automatic curryfication transformation, the real
fixpoint combinator is working on a sigma type of the arguments. 
Reduces to the previous impl in case only one argument is involved.
The patch also introduces a new flag on implicit arguments that says if
the argument has to be infered (default) or can be turned into a
subgoal/obligation. Comes with a test-suite file.


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

32 files changed, 357 insertions, 332 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 91a9eeefa..9723f2c22 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -873,7 +873,8 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
 and extern_recursion_order scopes vars = function
     RStructRec -> CStructRec
   | RWfRec c -> CWfRec (extern true scopes vars c)
-  | RMeasureRec c -> CMeasureRec (extern true scopes vars c)
+  | RMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m, 
+				     Option.map (extern true scopes vars) r)
 
 
 let extern_rawconstr vars c =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index a447fbe8d..172d032b5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -289,7 +289,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   let (vars1,unbndltacvars) = ltacvars in
   (* Is [id] an inductive type potentially with implicit *)
   try
-    let ty, l,impl,argsc = List.assoc id impls in
+    let ty,l,impl,argsc = List.assoc id impls in
     let l = List.map 
       (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
     let tys = string_of_ty ty in
@@ -298,8 +298,9 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
-  then
-    RVar (loc,id), [], [], []
+  then (
+    Dumpglob.dump_reference loc "<>" (string_of_id id) "var";
+    RVar (loc,id), [], [], [])
   (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
@@ -794,9 +795,9 @@ let check_projection isproj nargs r =
 let get_implicit_name n imps =
   Some (Impargs.name_of_implicit (List.nth imps (n-1)))
 
-let set_hole_implicit i = function
-  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i))
-  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i))
+let set_hole_implicit i b = function
+  | RRef (loc,r) -> (loc,Evd.ImplicitArg (r,i,b))
+  | RVar (loc,id) -> (loc,Evd.ImplicitArg (VarRef id,i,b))
   | _ -> anomaly "Only refs have implicits"
 
 let exists_implicit_name id =
@@ -857,7 +858,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	in
         let idl = Array.map
           (fun (id,(n,order),bl,ty,bd) ->
-	     let intern_ro_arg c f =
+	     let intern_ro_arg f =
 	       let idx = 
 		 match n with
 		     Some (loc, n) -> list_index0 (Name n) (List.map snd (names_of_local_assums bl))
@@ -866,22 +867,18 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	       let before, after = list_chop idx bl in
 	       let ((ids',_,_,_) as env',rbefore) =
 		 List.fold_left intern_local_binder (env,[]) before in
-	       let ro =
-		 match c with 
-		   | None -> RStructRec 
-		   | Some c' -> f (intern (ids', unb, tmp_scope, scopes) c') 
-	       in 
+	       let ro = f (intern (ids', unb, tmp_scope, scopes)) in 
 	       let n' = Option.map (fun _ -> List.length before) n in
 		 n', ro, List.fold_left intern_local_binder (env',rbefore) after
 	     in
 	     let n, ro, ((ids',_,_,_),rbl) =
-	       (match order with
-		 | CStructRec -> 
-		     intern_ro_arg None (fun _ -> RStructRec)
-		 | CWfRec c ->
-		     intern_ro_arg (Some c) (fun r -> RWfRec r)
-		 | CMeasureRec c ->
-		     intern_ro_arg (Some c) (fun r -> RMeasureRec r))
+	       match order with
+	       | CStructRec -> 
+		   intern_ro_arg (fun _ -> RStructRec)
+	       | CWfRec c ->
+		   intern_ro_arg (fun f -> RWfRec (f c))
+	       | CMeasureRec (m,r) ->
+		   intern_ro_arg (fun f -> RMeasureRec (f m, Option.map f r))
 	     in
 	     let ids'' = List.fold_right Idset.add lf ids' in
 	     ((n, ro), List.rev rbl, 
@@ -1153,7 +1150,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
             (* with implicit arguments if maximal insertion is set *)
 	    []
 	  else
-	    RHole (set_hole_implicit (n,get_implicit_name n l) c) :: 
+	    RHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) :: 
 	      aux (n+1) impl' subscopes' eargs rargs
 	  end
       | (imp::impl', a::rargs') ->
@@ -1216,7 +1213,7 @@ let intern_pattern env patt =
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
 
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
 
 (*********************************************************************)
 (* Functions to parse and interpret constructions *)
@@ -1354,7 +1351,7 @@ let interp_context_gen understand_type understand_judgment env bl =
 	      let impls = 
 		if k = Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
-		    (ExplByPos (n, na), (true, true)) :: impls
+		    (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
 		(push_rel d env, d::params, succ n, impls)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 126eff859..25bcc66b0 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -47,7 +47,7 @@ type var_internalisation_data =
 type implicits_env = (identifier * var_internalisation_data) list
 type full_implicits_env = identifier list * implicits_env
 
-type manual_implicits = (explicitation * (bool * bool)) list
+type manual_implicits = (explicitation * (bool * bool * bool)) list
 
 type ltac_sign = identifier list * unbound_ltac_var_map
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index a9d370447..4495c22c6 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -254,7 +254,7 @@ let implicits_of_rawterm l =
 		    Name id -> Some id
 		  | Anonymous -> None
 	      in
-		(ExplByPos (i, name), (true, true)) :: rest
+		(ExplByPos (i, name), (true, true, true)) :: rest
 	    else rest
       | RLetIn (loc, na, t, b) -> aux i b
       | _ -> []
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index dc83e2135..57eff0b86 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -42,7 +42,7 @@ val free_vars_of_rawconstr : ?bound:Idset.t -> rawconstr -> (Names.identifier *
 
 val make_fresh : Names.Idset.t -> Environ.env -> identifier -> identifier
 
-val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool)) list
+val implicits_of_rawterm : Rawterm.rawconstr -> (Topconstr.explicitation * (bool * bool * bool)) list
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e0a8ca600..666f9022b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -375,7 +375,7 @@ let rec subst_aconstr subst bound raw =
 
   | APatVar _ | ASort _ -> raw
 
-  | AHole (Evd.ImplicitArg (ref,i)) ->
+  | AHole (Evd.ImplicitArg (ref,i,b)) ->
       let ref',t = subst_global subst ref in 
 	if ref' == ref then raw else
 	  AHole (Evd.InternalHole)
@@ -683,7 +683,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
-  | CMeasureRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
 
 type constr_pattern_expr = constr_expr
 
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 303926967..1982a08fd 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -161,7 +161,7 @@ and cofixpoint_expr =
 and recursion_order_expr = 
   | CStructRec
   | CWfRec of constr_expr
-  | CMeasureRec of constr_expr
+  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
 
 (** Anonymous defs allowed ?? *)
 and local_binder =
diff --git a/library/impargs.ml b/library/impargs.ml
index be872d303..ebbd49ebc 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -242,7 +242,7 @@ let rec prepare_implicits f = function
   | (Anonymous, Some _)::_ -> anomaly "Unnamed implicit"
   | (Name id, Some imp)::imps -> 
       let imps' = prepare_implicits f imps in
-      Some (id,imp,set_maximality imps' f.maximal) :: imps'
+      Some (id,imp,(set_maximality imps' f.maximal,true)) :: imps'
   | _::imps -> None :: prepare_implicits f imps
 
 let compute_implicits_flags env f all t = 
@@ -265,10 +265,10 @@ let compute_manual_implicits env flags t enriching l =
   let n = List.length autoimps in
   let try_forced k l =
     try 
-      let (id, (b, f)), l' = assoc_by_pos k l in
-	if f then
+      let (id, (b, fi, fo)), l' = assoc_by_pos k l in
+	if fo then
 	  let id = match id with Some id -> id | None -> id_of_string ("arg_" ^ string_of_int k) in
-	    l', Some (id,Manual,b)
+	    l', Some (id,Manual,(b,fi))
 	else l, None
     with Not_found -> l, None
   in
@@ -279,17 +279,17 @@ let compute_manual_implicits env flags t enriching l =
   | (Name id,imp)::imps ->
       let l',imp,m =
 	try 
-	  let (b, f) = List.assoc (ExplByName id) l in
-	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some b)
+	  let (b, fi, fo) = List.assoc (ExplByName id) l in
+	  List.remove_assoc (ExplByName id) l, (Some Manual), (Some (b, fi))
 	with Not_found ->
 	try 
-	  let (id, (b, f)), l' = assoc_by_pos k l in
-	    l', (Some Manual), (Some b)
+	  let (id, (b, fi, fo)), l' = assoc_by_pos k l in
+	    l', (Some Manual), (Some (b,fi))
 	with Not_found ->
-	  l,imp, if enriching && imp <> None then Some flags.maximal else None
+	  l,imp, if enriching && imp <> None then Some (flags.maximal,true) else None
       in
       let imps' = merge (k+1) l' imps in
-      let m = Option.map (set_maximality imps') m in
+      let m = Option.map (fun (b,f) -> set_maximality imps' b, f) m in
       Option.map (set_implicit id imp) m :: imps'
   | (Anonymous,imp)::imps ->
       let l', forced = try_forced k l in
@@ -297,7 +297,7 @@ let compute_manual_implicits env flags t enriching l =
   | [] when l = [] -> []
   | [] ->
       List.iter (function 
-	| ExplByName id,(b,forced) -> 
+	| ExplByName id,(b,fi,forced) -> 
 	    if not forced then
 	      error ("Wrong or not dependent implicit argument name: "^(string_of_id id))
 	| ExplByPos (i,_id),_t ->
@@ -324,10 +324,11 @@ let compute_implicits_auto env f manual t =
 let compute_implicits env t = compute_implicits_auto env !implicit_args [] t
 
 type maximal_insertion = bool (* true = maximal contextual insertion *)
+type force_inference = bool (* true = always infer, never turn into evar/subgoal *)
 
 type implicit_status =
     (* None = Not implicit *)
-    (identifier * implicit_explanation * maximal_insertion) option
+    (identifier * implicit_explanation * (maximal_insertion * force_inference)) option
 
 type implicits_list = implicit_status list
 
@@ -340,7 +341,11 @@ let name_of_implicit = function
   | Some (id,_,_) -> id
 
 let maximal_insertion_of = function
-  | Some (_,_,b) -> b
+  | Some (_,_,(b,_)) -> b
+  | None -> anomaly "Not an implicit argument"
+
+let force_inference_of = function
+  | Some (_, _, (_, b)) -> b
   | None -> anomaly "Not an implicit argument"
 
 (* [in_ctx] means we know the expected type, [n] is the index of the argument *)
@@ -462,7 +467,7 @@ let subst_implicits (_,subst,(req,l)) =
   (ImplLocal,list_smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, true) else None)
+  List.rev_map (fun (id,impl,_,_) -> if impl = Lib.Implicit then Some (id, Manual, (true,true)) else None)
     (List.filter (fun (_,_,b,_) -> b = None) ctx)
 
 let section_segment_of_reference = function
@@ -566,7 +571,7 @@ let declare_mib_implicits kn =
       (inImplicits (ImplMutualInductive (kn,flags),List.flatten imps))
 
 (* Declare manual implicits *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool) 
+type manual_explicitation = Topconstr.explicitation * (bool * bool * bool) 
 
 let compute_implicits_with_manual env typ enriching l = 
   compute_manual_implicits env !implicit_args typ enriching l
diff --git a/library/impargs.mli b/library/impargs.mli
index 0eba9f380..472eeb031 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -52,13 +52,14 @@ type implicit_explanation =
   | DepFlexAndRigid of (*flex*) argument_position * (*rig*) argument_position
   | Manual
 
-type implicit_status = (identifier * implicit_explanation * bool) option
+type implicit_status = (identifier * implicit_explanation * (bool * bool)) option
 type implicits_list = implicit_status list
 
 val is_status_implicit : implicit_status -> bool
 val is_inferable_implicit : bool -> int -> implicit_status -> bool
 val name_of_implicit : implicit_status -> identifier
 val maximal_insertion_of : implicit_status -> bool
+val force_inference_of : implicit_status -> bool
 
 val positions_of_implicits : implicits_list -> int list
 
@@ -67,8 +68,8 @@ val positions_of_implicits : implicits_list -> int list
 val compute_implicits : env -> types -> implicits_list
 
 (* A [manual_explicitation] is a tuple of a positional or named explicitation with
-   maximal insertion and forcing flags. *)
-type manual_explicitation = Topconstr.explicitation * (bool * bool)
+   maximal insertion, force inference and force usage flags. *)
+type manual_explicitation = Topconstr.explicitation * (bool * bool * bool)
 
 val compute_implicits_with_manual : env -> types -> bool -> 
   manual_explicitation list -> implicits_list
@@ -112,14 +113,3 @@ type implicit_discharge_request =
   | ImplInteractive of global_reference * implicits_flags * 
       implicit_interactive_request
 
-val discharge_implicits :     'a *
-    (implicit_discharge_request *
-     (Libnames.global_reference *
-      (Names.identifier * implicit_explanation * bool) option list)
-     list) ->
-    (implicit_discharge_request *
-     (Libnames.global_reference *
-      (Names.identifier * implicit_explanation * bool) option list)
-     list)
-    option
-
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 37c09704e..9152083bf 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -397,7 +397,8 @@ GEXTEND Gram
   fixannot:
     [ [ "{"; IDENT "struct"; id=identref; "}" -> (Some id, CStructRec)
     | "{"; IDENT "wf"; rel=constr; id=OPT identref; "}" -> (id, CWfRec rel)
-    | "{"; IDENT "measure"; rel=constr; id=OPT identref; "}" -> (id, CMeasureRec rel)
+    | "{"; IDENT "measure"; m=constr; id=OPT identref; 
+	rel = OPT [ "on"; r=constr -> r ]; "}" -> (id, CMeasureRec (m,rel))
     ] ]
   ;
   binders_let_fixannot:
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index e1e334be6..3a57fd545 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -57,6 +57,9 @@ END
 
 (* Errors *)
 
+let error_expect_two_arguments loc =
+  user_err_loc (loc,"",str "wrong number of arguments (expect two).")
+
 let error_expect_one_argument loc =
   user_err_loc (loc,"",str "wrong number of arguments (expect one).")
 
@@ -241,8 +244,8 @@ and interp_xml_recursionOrder x =
 	     | _ -> error_expect_one_argument loc)
       | "Measure" -> 
 	  (match l with
-	       [c] -> RMeasureRec (interp_xml_type c)
-	     | _ -> error_expect_one_argument loc)
+	       [m;r] -> RMeasureRec (interp_xml_type m, Some (interp_xml_type r))
+	     | _ -> error_expect_two_arguments loc)
       | _ ->
           user_err_loc (locs,"",str "Invalid recursion order.")
 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index e16641a83..828289585 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -406,8 +406,9 @@ let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
 	  else mt() 
       | CWfRec c ->
 	  spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
-      | CMeasureRec c ->
-	  spc () ++ str "{measure " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
+      | CMeasureRec (m,r) ->
+	  spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++ 
+	    (match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}"
   in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 4eb8ae938..0054326e4 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -636,9 +636,10 @@ let rec pr_vernac = function
 		      | CWfRec c -> 
 			  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++ 
 			    pr_id id ++ str"}"
-		      | CMeasureRec c -> 
-			  spc() ++ str "{measure " ++ pr_lconstr_expr c ++ spc() ++ 
-			    pr_id id ++ str"}"
+		      | CMeasureRec (m,r) -> 
+			  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++ 
+			    pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++ 
+			    pr_lconstr_expr r) ++ str"}"
 	    in
             pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index e59de34a4..378f9972e 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -88,7 +88,7 @@ let trd_of_3 (_, _, x) = x
    prooftree will also depend on things like tactic declarations, etc
    so we may need a new type for that. *)
 let rec depends_of_hole_kind hk acc = match hk with
-  | Evd.ImplicitArg (gr,_)            -> gr::acc
+  | Evd.ImplicitArg (gr,_,_)            -> gr::acc
   | Evd.TomatchTypeParameter (ind, _) -> (IndRef ind)::acc
   | Evd.BinderType _
   | Evd.QuestionMark _
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 04f57331d..6d2902c61 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -111,7 +111,7 @@ let interp_context_evars evdref env params =
 	      let impls = 
 		if k = Implicit then
 		  let na = match na with Name n -> Some n | Anonymous -> None in
-		    (ExplByPos (n, na), (true, true)) :: impls
+		    (ExplByPos (n, na), (true, true, true)) :: impls
 		else impls
 	      in
 		(push_rel d env, d::params, succ n, impls)
@@ -180,123 +180,134 @@ let split_args n rel = match list_chop ((List.length rel) - n) rel with
     (l1, x :: l2) -> l1, x, l2
   | _ -> assert(false)
 
-let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+open Coqlib
+
+let sigT = Lazy.lazy_from_fun build_sigma_type
+let sigT_info = lazy
+  { ci_ind       = destInd (Lazy.force sigT).typ;
+    ci_npar      = 2;
+    ci_cstr_nargs = [|2|];
+    ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
+  }
+
+let telescope = function
+  | [] -> assert false
+  | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
+  | (n, None, t) :: tl ->
+      let ty, tys, (k, constr) =
+	List.fold_left
+	  (fun (ty, tys, (k, constr)) (n, b, t) -> 
+	    let pred = mkLambda (n, t, ty) in
+	    let sigty = mkApp ((Lazy.force sigT).typ, [|t; pred|]) in
+	    let intro = mkApp ((Lazy.force sigT).intro, [|lift k t; lift k pred; mkRel k; constr|]) in
+	      (sigty, pred :: tys, (succ k, intro)))
+	  (t, [], (2, mkRel 1)) tl
+      in
+      let (last, subst) = List.fold_right2
+	(fun pred (n, b, t) (prev, subst) ->
+	  let proj1 = applistc (Lazy.force sigT).proj1 [t; pred; prev] in
+	  let proj2 = applistc (Lazy.force sigT).proj2 [t; pred; prev] in
+	    (lift 1 proj2, (n, Some proj1, t) :: subst))
+	(List.rev tys) tl (mkRel 1, [])
+      in ty, ((n, Some last, t) :: subst), constr
+      
+  | _ -> raise (Invalid_argument "telescope")
+
+let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let sigma = Evd.empty in
   let isevars = ref (Evd.create_evar_defs sigma) in
   let env = Global.env() in 
-  let pr c = my_print_constr env c in
-  let prr = Printer.pr_rel_context env in
+  let _pr c = my_print_constr env c in
+  let _prr = Printer.pr_rel_context env in
   let _prn = Printer.pr_named_context env in
   let _pr_rel env = Printer.pr_rel_context env in
-(*   let _ =  *)
-(*     try debug 2 (str "In named context: " ++ prn (named_context env) ++ str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++  *)
-(* 		 Ppconstr.pr_binders bl ++ str " : " ++  *)
-(* 		 Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ *)
-(* 		 Ppconstr.pr_constr_expr body) *)
-(*     with _ -> () *)
-    (*   in *)
   let (env', binders_rel), impls = interp_context_evars isevars env bl in
-  let after, ((argname, _, argtyp) as arg), before = 
-    let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
-      split_args idx binders_rel in
-  let before_length, after_length = List.length before, List.length after in
-  let argid = match argname with Name n -> n | _ -> assert(false) in
-  let liftafter = lift_binders 1 after_length after in
-  let envwf = push_rel_context before env in
-  let wf_rel, wf_rel_fun, measure_fn = 
-    let rconstr_body, rconstr = 
-      let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
-      let env = push_rel_context [arg] envwf in
-      let capp = interp_constr isevars env app in
- 	capp, mkLambda (argname, argtyp, capp)
-    in
-      trace (str"rconstr_body: " ++ pr rconstr_body);
-      if measure then
- 	let lt_rel = constr_of_global (Lazy.force lt_ref) in
- 	let name s = Name (id_of_string s) in
- 	let wf_rel_fun lift x y = (* lift to before_env *)
-	  trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body));
- 	  mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); 
- 			    subst1 y (liftn lift 2 rconstr_body) |])
-	in
- 	let wf_rel = 
- 	  mkLambda (name "x", argtyp,
- 		    mkLambda (name "y", lift 1 argtyp,
- 			      wf_rel_fun 0 (mkRel 2) (mkRel 1)))
- 	in
- 	  wf_rel, wf_rel_fun , Some rconstr
-       else rconstr, (fun lift x y -> mkApp (rconstr, [|x; y|])), None
+  let len = List.length binders_rel in
+  let top_env = push_rel_context binders_rel env in
+  let top_arity = interp_type_evars isevars top_env arityc in
+  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
+  let argtyp, letbinders, make = telescope binders_rel in
+  let argname = id_of_string "recarg" in
+  let arg = (Name argname, None, argtyp) in
+  let wrapper x = 
+    if List.length binders_rel > 1 then 
+      it_mkLambda_or_LetIn (mkApp (x, [|make|])) binders_rel
+    else x
   in
-  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
+  let binders = letbinders @ [arg] in
+  let binders_env = push_rel_context binders_rel env in
+  let rel = interp_constr isevars env r in
+  let measure = interp_constr isevars binders_env measure in
+  let measure_ty = type_of binders_env !isevars measure in
+  let wf_rel, wf_rel_fun, measure_fn =
+    let measure_body, measure =
+      it_mkLambda_or_LetIn measure letbinders,
+      it_mkLambda_or_LetIn measure binders
+    in
+    let comb = constr_of_global (Lazy.force measure_on_R_ref) in
+    let wf_rel = mkApp (comb, [| argtyp; measure_ty; rel; measure |]) in 
+    let wf_rel_fun x y =
+      mkApp (rel, [| subst1 x measure_body;
+ 		     subst1 y measure_body |])
+    in wf_rel, wf_rel_fun, measure
   in
-  let argid' = id_of_string (string_of_id argid ^ "'") in
+  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |]) in
+  let argid' = id_of_string (string_of_id argname ^ "'") in
   let wfarg len = (Name argid', None,
-  		   mkSubset (Name argid') (lift len argtyp) 
-		     (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
+  		  mkSubset (Name argid') argtyp
+		    (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
   in
-  let top_bl = after @ (arg :: before) in
-  let top_env = push_rel_context top_bl env in
-  let top_arity = interp_type_evars isevars top_env arityc in
-  let intern_bl = wfarg 1 :: arg :: before in
+  let intern_bl = wfarg 1 :: [arg] in
   let _intern_env = push_rel_context intern_bl env in
   let proj = (Lazy.force sig_).Coqlib.proj1 in
+  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
   let projection = (* in wfarg :: arg :: before *)
-    mkApp (proj, [| argtyp ;
-		    (mkLambda (Name argid', argtyp,
-			      (wf_rel_fun 3 (mkRel 1) (mkRel 3)))) ;
-		    mkRel 1
-		 |])
+    mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
   in
-  let intern_arity = it_mkProd_or_LetIn top_arity after in
-  (* Intern arity is in top_env = arg :: before *)
-  let intern_arity = liftn 2 2 intern_arity in
-(*     trace (str "After lifting arity: " ++  *)
-(* 	      my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
-(* 	      intern_arity); *)
-  (* arity is now in something :: wfarg :: arg :: before 
-     where what refered to arg now refers to something *)
-  let intern_arity = substl [projection] intern_arity in
-  (* substitute the projection of wfarg for something, 
-     now intern_arity is in wfarg :: arg :: before *)
+  let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in 
+  let intern_arity = substl [projection] top_arity_let in
+  (* substitute the projection of wfarg for something,
+     now intern_arity is in wfarg :: arg *)
   let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
-  let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
-  let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
-  let fun_env = push_rel_context fun_bl envwf in
-  let fun_arity = interp_type_evars isevars fun_env arityc in
-  let intern_body = interp_casted_constr isevars fun_env body fun_arity in
-  let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
-  let _ =
-    try trace ((* str "Fun bl: " ++ prr fun_bl ++ spc () ++ *)
-		 str "Intern bl" ++ prr intern_bl ++ spc ())
-(* 		 str "Top bl" ++ prr top_bl ++ spc () ++ *)
-(* 		 str "Intern arity: " ++ pr intern_arity ++ *)
-(* 		 str "Top arity: " ++ pr top_arity ++ spc () ++ *)
-(* 		   str "Intern body " ++ pr intern_body_lam) *)
-    with _ -> ()
+  let intern_fun_binder = (Name (add_suffix recname "'"), None, intern_fun_arity_prod) in
+  let curry_fun = 
+    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
+    let arg = mkApp ((Lazy.force sig_).intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
+    let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
+    let rcurry = mkApp (rel, [| measure; lift len measure |]) in
+    let lam = (Name (id_of_string "recproof"), None, rcurry) in
+    let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
+    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
+      (Name recname, Some body, ty)
+  in
+  let fun_bl = intern_fun_binder :: [arg] in
+  let lift_lets = Termops.lift_rel_context 1 letbinders in
+  let intern_body = 
+    let ctx = (Name recname, None, pi3 curry_fun) :: binders_rel in
+    let impls = Command.compute_interning_datas env Constrintern.Recursive [] [recname] [full_arity] [impls] in
+    let newimpls = 
+      match snd impls with
+      [(p, (r, l, impls, scopes))] ->
+	[(p, (r, l, impls @ [Some (id_of_string "recproof", Impargs.Manual, (true, false))], scopes @ [None]))]
+      | x -> x
+    in interp_casted_constr isevars ~impls:(fst impls,newimpls) 
+      (push_rel_context ctx env) body (lift 1 top_arity)
   in
-  let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
-    (* Lift to get to constant arguments *)
-(*   let lift_cst = List.length after + 1 in *)
+  let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
+  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
   let fix_def =
-    match measure_fn with
-	None ->
-	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
-		 [| argtyp ;
-		    wf_rel ;
-		    make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
-		    prop ; intern_body_lam |])
-      | Some f ->
-	  mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
-		[| argtyp ; f ; prop ; intern_body_lam |])
+    mkApp (constr_of_global (Lazy.force fix_sub_ref),
+	  [| argtyp ; wf_rel ; 
+	     make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
+	     prop ; intern_body_lam |])
   in
-  let def_appl = (* applist (fix_def, gen_rels (after_length + 1)) *) fix_def in
-  let def = it_mkLambda_or_LetIn def_appl before in
+  let def = wrapper fix_def in
   let typ = it_mkProd_or_LetIn top_arity binders_rel in
   let fullcoqc = Evarutil.nf_isevar !isevars def in
   let fullctyp = Evarutil.nf_isevar !isevars typ in
-  let evm =evars_of_term ( !isevars) Evd.empty fullctyp in
-  let evm = evars_of_term ( !isevars) evm fullcoqc in
+  let evm = evars_of_term !isevars Evd.empty fullctyp in
+  let evm = evars_of_term !isevars evm fullcoqc in
   let evm = non_instanciated_map env isevars evm in
   let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
     Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
@@ -442,10 +453,15 @@ let build_recursive l b =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
 	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
-
-      | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
-	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false)
+	  ignore(build_wellfounded (id, n, bl, typ, def) r 
+		    (match n with Some n -> mkIdentC (snd n) | None -> 
+		      errorlabstrm "Subtac_command.build_recursive"
+			(str "Recursive argument required for well-founded fixpoints"))
+		    ntn false)
+
+      | [(n, CMeasureRec (m, r))], [(((_,id),_,bl,typ,def),ntn)] ->
+	  ignore(build_wellfounded (id, n, bl, typ, def) (Option.default (CRef lt_ref) r)
+		    m ntn false)
 
       | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
 	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> 
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 8b8bb9ab4..c1097375b 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -53,7 +53,7 @@ type program_info = {
   prg_obligations: obligations;
   prg_deps : identifier list;
   prg_fixkind : Command.fixpoint_kind option ;
-  prg_implicits : (Topconstr.explicitation * (bool * bool)) list;
+  prg_implicits : (Topconstr.explicitation * (bool * bool * bool)) list;
   prg_notations : notations ;
   prg_kind : definition_kind;
   prg_hook : definition_hook;
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index 60c0a4139..de6796b2f 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -24,7 +24,7 @@ val get_proofs_transparency : unit -> bool
 type definition_hook = global_reference -> unit
 
 val add_definition : Names.identifier ->  Term.constr -> Term.types -> 
-  ?implicits:(Topconstr.explicitation * (bool * bool)) list ->
+  ?implicits:(Topconstr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:Proof_type.tactic ->
   ?hook:definition_hook -> obligation_info -> progress
@@ -33,7 +33,7 @@ type notations = (string * Topconstr.constr_expr * Topconstr.scope_name option)
 
 val add_mutual_definitions : 
   (Names.identifier * Term.constr * Term.types *
-      (Topconstr.explicitation * (bool * bool)) list * obligation_info) list -> 
+      (Topconstr.explicitation * (bool * bool * bool)) list * obligation_info) list -> 
   ?tactic:Proof_type.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   notations ->
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index ba30ee190..8e38999fd 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -29,12 +29,12 @@ let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
 let acc_ref = make_ref  ["Init";"Wf"] "Acc"
 let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
 let fix_sub_ref = make_ref fixsub_module "Fix_sub"
+let measure_on_R_ref = make_ref fixsub_module "MR"
 let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
-let lt_ref = make_ref ["Init";"Peano"] "lt"
-let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
 let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
 
 let make_ref s = Qualid (dummy_loc, qualid_of_string s)
+let lt_ref = make_ref "Init.Peano.lt"
 let sig_ref = make_ref "Init.Specif.sig"
 let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
 let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -199,10 +199,11 @@ let non_instanciated_map env evd evm =
 	 debug 2 (str "evar " ++ int key ++ str " has kind " ++ 
 		    str (string_of_hole_kind k));
 	 match k with 
-	     QuestionMark _ -> Evd.add evm key evi
-	   | _ ->
-	       debug 2 (str " and is an implicit");
-	       Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
+	 | QuestionMark _ -> Evd.add evm key evi
+	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
+	 | _ ->
+	     debug 2 (str " and is an implicit");
+	     Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
     Evd.empty (Evarutil.non_instantiated evm)
     
 let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index 964f668f2..d60893283 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -24,10 +24,10 @@ val well_founded_ref : global_reference lazy_t
 val acc_ref : global_reference lazy_t
 val acc_inv_ref : global_reference lazy_t
 val fix_sub_ref : global_reference lazy_t
+val measure_on_R_ref : global_reference lazy_t
 val fix_measure_sub_ref : global_reference lazy_t
-val lt_ref : global_reference lazy_t
-val lt_wf_ref : global_reference lazy_t
 val refl_ref : global_reference lazy_t
+val lt_ref : reference
 val sig_ref : reference
 val proj1_sig_ref : reference
 val proj2_sig_ref : reference
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 6854a4a7c..b2e9f0e6b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -654,7 +654,7 @@ let rec subst_rawconstr subst raw =
 
   | RSort _ -> raw
 
-  | RHole (loc,ImplicitArg (ref,i)) ->
+  | RHole (loc,ImplicitArg (ref,i,b)) ->
       let ref',_ = subst_global subst ref in 
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 6bc77abcb..79bbbf10e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -410,7 +410,7 @@ let metamap_to_list m =
 type obligation_definition_status = Define of bool | Expand
 
 type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option)
+  | ImplicitArg of global_reference * (int * identifier option) * bool
   | BinderType of name
   | QuestionMark of obligation_definition_status
   | CasesType
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ac708d1ec..406914440 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -169,7 +169,7 @@ type obligation_definition_status = Define of bool | Expand
 
 (* Evars *)
 type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option)
+  | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *)
   | BinderType of name
   | QuestionMark of obligation_definition_status
   | CasesType
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 4d3348407..d8eae2d0d 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -75,7 +75,7 @@ type rawconstr =
 
 and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 3628e2a50..6bb4eceb3 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -79,7 +79,7 @@ type rawconstr =
 
 and rawdecl = name * binding_kind * rawconstr option * rawconstr
 
-and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr
+and fix_recursion_order = RStructRec | RWfRec of rawconstr | RMeasureRec of rawconstr * rawconstr option
 
 and fix_kind =
   | RFix of ((int option * fix_recursion_order) array * int)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 38e4fb677..56b78715a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -277,7 +277,7 @@ let is_instance = function
 
 let is_implicit_arg k = 
   match k with
-      ImplicitArg (ref, (n, id)) -> true
+      ImplicitArg (ref, (n, id), b) -> true
     | InternalHole -> true
     | _ -> false
 
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
new file mode 100644
index 000000000..8cf97b03f
--- /dev/null
+++ b/test-suite/success/ProgramWf.v
@@ -0,0 +1,103 @@
+Require Import Arith Program.
+Set Implicit Arguments.
+(* Set Printing All. *)
+Print sigT_rect.
+Obligation Tactic := program_simplify ; auto with *.
+
+Program Fixpoint merge (n m : nat) {measure (n + m) on lt} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+
+Print merge.
+
+Require Import ZArith.
+
+
+Print Zlt. 
+Require Import Zwf.
+Print Zwf.
+
+Open Local Scope Z_scope.
+
+Program Fixpoint Zwfrec (n m : Z) {measure (n + m) on (Zwf 0)} : Z :=
+  match n ?= m with
+    | Lt => Zwfrec n (Zpred m)
+    | _ => 0
+  end.
+
+Next Obligation. 
+  red. Admitted.
+
+Close Scope Z_scope.
+
+Program Fixpoint merge_wf (n m : nat) {wf lt m} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+
+Print merge_wf.
+
+Program Fixpoint merge_one (n : nat) {measure n} : nat :=
+  match n with
+    | 0 => 0
+    | S n' => merge_one n'
+  end.
+
+Print Hint well_founded.
+Print merge_one. Eval cbv delta [merge_one] beta zeta in merge_one.
+
+Import WfExtensionality.
+
+Lemma merge_unfold n m : merge n m = 
+  match n with
+    | 0 => 0
+    | S n' => merge n' m
+  end.
+Proof. intros. unfold_sub merge (merge n m). simpl. destruct n ; reflexivity. Qed.
+
+Print merge.
+
+Require Import Arith.
+Unset Implicit Arguments.
+
+Time Program Fixpoint check_n  (n : nat) (P : { i | i < n } -> bool) (p : nat)
+  (H : forall (i : { i | i < n }), i < p -> P i = true)
+  {measure (n - p)} : 
+  Exc (forall (p : { i | i < n}), P p = true) :=
+  match le_lt_dec n p with
+  | left _ => value _
+  | right cmp =>
+      if dec (P p) then
+        check_n n P (S p) _
+      else
+        error
+  end.
+
+Require Import Omega Setoid.
+
+Next Obligation. 
+  intros ; simpl in *. apply H. 
+  simpl in * ; omega.
+Qed.
+
+Next Obligation. simpl in *; intros. 
+  revert H0 ; clear_subset_proofs. intros. 
+  case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst. 
+  revert H0 ; clear_subset_proofs ; tauto.
+
+  apply H. simpl. omega.
+Qed.
+
+Print check_n.
+Print sigT_rect.
+Print check_n.
+
+Program Fixpoint check_n'  (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p)
+  {measure (p - n) p} : nat :=
+  _.
+
+Print Opaque Dependencies check_n.
+
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index ff407182d..aa653de0f 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -145,8 +145,3 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
     end }.
 
   Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
-
-  Next Obligation.
-  Proof. clear aux. red in H0. subst. 
-    destruct y; intuition (discriminate || eauto).
-  Defined.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b058f67ba..c690ee4a7 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -306,17 +306,13 @@ Notation "∙⊥∙" := false_predicate : predicate_scope.
 
 (** Predicate equivalence is an equivalence, and predicate implication defines a preorder. *)
 
-Program Instance predicate_equivalence_equivalence :
-  Equivalence (@predicate_equivalence l).
-
+Program Instance predicate_equivalence_equivalence : Equivalence (@predicate_equivalence l).
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-  
   Next Obligation.
     fold pointwise_lifting.
     induction l. firstorder.
@@ -326,11 +322,9 @@ Program Instance predicate_equivalence_equivalence :
 
 Program Instance predicate_implication_preorder :
   PreOrder (@predicate_implication l).
-
   Next Obligation.
     induction l ; firstorder.
   Qed.
-
   Next Obligation.
     induction l. firstorder.
     unfold predicate_implication in *. simpl in *. 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 5d005d273..497e60205 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -85,78 +85,6 @@ End Well_founded.
 
 Extraction Inline Fix_F_sub Fix_sub.
 
-Require Import Wf_nat.
-Require Import Lt.
-
-Section Well_founded_measure.
-  Variable A : Type.
-  Variable m : A -> nat.
-  
-  Section Acc.
-    
-    Variable P : A -> Type.
-    
-    Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x.
-    
-    Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x :=
-      F_sub x (fun (y : A | m y < m x)  => Fix_measure_F_sub y
-        (@Acc_inv _ _ _ r (m y) (proj2_sig y))).
-    
-    Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)).
-  
-  End Acc.
-
-  Section FixPoint.
-    Variable P : A -> Type.
-    
-    Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x.
-    
-    Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *)
-    
-    Definition Fix_measure (x:A) := Fix_measure_F_sub P F_sub x (lt_wf (m x)).
-    
-    Hypothesis
-      F_ext :
-      forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)),
-        (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g.
-
-    Program Lemma Fix_measure_F_eq :
-      forall (x:A) (r:Acc lt (m x)),
-        F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r.
-    Proof.
-      intros x.
-      set (y := m x).
-      unfold Fix_measure_F_sub.
-      intros r ; case r ; auto.
-    Qed.
-    
-    Lemma Fix_measure_F_inv : forall (x:A) (r s:Acc lt (m x)), Fix_F x r = Fix_F x s.
-    Proof.
-      intros x r s.
-      rewrite (proof_irrelevance (Acc lt (m x)) r s) ; auto.
-    Qed.
-
-    Lemma Fix_measure_eq : forall x:A, Fix_measure x = F_sub x (fun (y:{y:A| m y < m x}) => Fix_measure (proj1_sig y)).
-    Proof.
-      intro x; unfold Fix_measure in |- *.
-      rewrite <- (Fix_measure_F_eq ).
-      apply F_ext; intros.
-      apply Fix_measure_F_inv.
-    Qed.
-
-    Lemma fix_measure_sub_eq : forall x : A,
-      Fix_measure_sub P F_sub x =
-        let f_sub := F_sub in
-          f_sub x (fun (y : A | m y < m x) => Fix_measure (`y)).
-      exact Fix_measure_eq.
-    Qed.
-
- End FixPoint.
-
-End Well_founded_measure.
-
-Extraction Inline Fix_measure_F_sub Fix_measure_sub.
-
 Set Implicit Arguments.
 
 (** Reasoning about well-founded fixpoints on measures. *)
@@ -165,7 +93,7 @@ Section Measure_well_founded.
 
   (* Measure relations are well-founded if the underlying relation is well-founded. *)
 
-  Variables T M: Set.
+  Variables T M: Type.
   Variable R: M -> M -> Prop.
   Hypothesis wf: well_founded R.
   Variable m: T -> M.
@@ -189,38 +117,41 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
-Section Fix_measure_rects.
+Hint Resolve measure_wf.
+
+Section Fix_rects.
 
   Variable A: Set.
-  Variable m: A -> nat.
   Variable P: A -> Type.
-  Variable f: forall (x : A), (forall y: { y: A | m y < m x }, P (proj1_sig y)) -> P x.
+  Variable R : A -> A -> Prop.
+  Variable Rwf : well_founded R.
+  Variable f: forall (x : A), (forall y: { y: A | R y x }, P (proj1_sig y)) -> P x.
   
   Lemma F_unfold x r:
-    Fix_measure_F_sub A m P f x r =
-    f (fun y => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
+    Fix_F_sub A R P f x r =
+    f (fun y => Fix_F_sub A R P f (proj1_sig y) (Acc_inv r (proj2_sig y))).
   Proof. intros. case r; auto. Qed.
 
-  (* Fix_measure_F_sub_rect lets one prove a property of
-  functions defined using Fix_measure_F_sub by showing
+  (* Fix_F_sub_rect lets one prove a property of
+  functions defined using Fix_F_sub by showing
   that property to be invariant over single application of the
   function body (f in our case). *)
 
-  Lemma Fix_measure_F_sub_rect
+  Lemma Fix_F_sub_rect
     (Q: forall x, P x -> Type)
     (inv: forall x: A,
-     (forall (y: A) (H: MR lt m y x) (a: Acc lt (m y)),
-        Q y (Fix_measure_F_sub A m P f y a)) ->
-        forall (a: Acc lt (m x)),
-          Q x (f (fun y: {y: A | m y < m x} =>
-            Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
-    : forall x a, Q _ (Fix_measure_F_sub A m P f x a).
+     (forall (y: A) (H: R y x) (a: Acc R y),
+        Q y (Fix_F_sub A R P f y a)) ->
+        forall (a: Acc R x),
+          Q x (f (fun y: {y: A | R y x} =>
+            Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y)))))
+    : forall x a, Q _ (Fix_F_sub A R P f x a).
   Proof with auto.
     intros Q inv.
-    set (R := fun (x: A) => forall a, Q _ (Fix_measure_F_sub A m P f x a)).
-    cut (forall x, R x)...
-    apply (well_founded_induction_type (measure_wf lt_wf m)).
-    subst R.
+    set (R' := fun (x: A) => forall a, Q _ (Fix_F_sub A R P f x a)).
+    cut (forall x, R' x)...
+    apply (well_founded_induction_type Rwf).
+    subst R'.
     simpl.
     intros.
     rewrite F_unfold...
@@ -229,29 +160,29 @@ Section Fix_measure_rects.
   (* Let's call f's second parameter its "lowers" function, since it
   provides it access to results for inputs with a lower measure.
 
-  In preparation of lemma similar to Fix_measure_F_sub_rect, but
-  for Fix_measure_sub, we first
+  In preparation of lemma similar to Fix_F_sub_rect, but
+  for Fix_sub, we first
   need an extra hypothesis stating that the function body has the
   same result for different "lowers" functions (g and h below) as long
   as those produce the same results for lower inputs, regardless
   of the lt proofs. *)
 
   Hypothesis equiv_lowers:
-    forall x0 (g h: forall x: {y: A | m y < m x0}, P (proj1_sig x)),
-    (forall x p p', g (exist (fun y: A => m y < m x0) x p) = h (exist _ x p')) ->
+    forall x0 (g h: forall x: {y: A | R y x0}, P (proj1_sig x)),
+    (forall x p p', g (exist (fun y: A => R y x0) x p) = h (exist _ x p')) ->
       f g = f h.
 
   (* From equiv_lowers, it follows that
-   [Fix_measure_F_sub A m P f x] applications do not not
+   [Fix_F_sub A R P f x] applications do not not
   depend on the Acc proofs. *)
 
-  Lemma eq_Fix_measure_F_sub x (a a': Acc lt (m x)):
-    Fix_measure_F_sub A m P f x a =
-    Fix_measure_F_sub A m P f x a'.
+  Lemma eq_Fix_F_sub x (a a': Acc R x):
+    Fix_F_sub A R P f x a =
+    Fix_F_sub A R P f x a'.
   Proof.
     intros x a.
-    pattern x, (Fix_measure_F_sub A m P f x a).
-    apply Fix_measure_F_sub_rect.
+    pattern x, (Fix_F_sub A R P f x a).
+    apply Fix_F_sub_rect.
     intros.
     rewrite F_unfold.
     apply equiv_lowers.
@@ -260,32 +191,34 @@ Section Fix_measure_rects.
     assumption.
   Qed.
 
-  (* Finally, Fix_measure_F_rect lets one prove a property of
-  functions defined using Fix_measure_F by showing that
+  (* Finally, Fix_F_rect lets one prove a property of
+  functions defined using Fix_F by showing that
   property to be invariant over single application of the function
   body (f). *)
 
-  Lemma Fix_measure_sub_rect
+  Lemma Fix_sub_rect
     (Q: forall x, P x -> Type)
     (inv: forall
       (x: A)
-      (H: forall (y: A), MR lt m y x -> Q y (Fix_measure_sub A m P f y))
-      (a: Acc lt (m x)),
-        Q x (f (fun y: {y: A | m y < m x} => Fix_measure_sub A m P f (proj1_sig y))))
-    : forall x, Q _ (Fix_measure_sub A m P f x).
+      (H: forall (y: A), R y x -> Q y (Fix_sub A R Rwf P f y))
+      (a: Acc R x),
+        Q x (f (fun y: {y: A | R y x} => Fix_sub A R Rwf P f (proj1_sig y))))
+    : forall x, Q _ (Fix_sub A R Rwf P f x).
   Proof with auto.
-    unfold Fix_measure_sub.
+    unfold Fix_sub.
     intros.
-    apply Fix_measure_F_sub_rect.
+    apply Fix_F_sub_rect.
     intros.
-    assert (forall y: A, MR lt m y x0 -> Q y (Fix_measure_F_sub A m P f y (lt_wf (m y))))...
+    assert (forall y: A, R y x0 -> Q y (Fix_F_sub A R P f y (Rwf y)))...
     set (inv x0 X0 a). clearbody q.
-    rewrite <- (equiv_lowers (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (lt_wf (m (proj1_sig y)))) (fun y: {y: A | m y < m x0} => Fix_measure_F_sub A m P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
+    rewrite <- (equiv_lowers (fun y: {y: A | R y x0} => 
+      Fix_F_sub A R P f (proj1_sig y) (Rwf (proj1_sig y))) 
+    (fun y: {y: A | R y x0} => Fix_F_sub A R P f (proj1_sig y) (Acc_inv a (proj2_sig y))))...
     intros.
-    apply eq_Fix_measure_F_sub.
+    apply eq_Fix_F_sub.
   Qed.
 
-End Fix_measure_rects.
+End Fix_rects.
 
 (** Tactic to fold a definitions based on [Fix_measure_sub]. *)
 
@@ -293,7 +226,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] => 
       match T with
-        appcontext C [ @Fix_measure_sub _ _ _ _ ?arg ] => 
+        appcontext C [ @Fix_sub _ _ _ _ ?arg ] => 
         let app := context C [ f arg ] in
           change app
       end
@@ -325,27 +258,11 @@ Module WfExtensionality.
     extensionality y ; apply H.
     rewrite H0 ; auto.
   Qed.
-
-  (** For a function defined with Program using a measure. *)
-  
-  Program Lemma fix_sub_measure_eq_ext :
-    forall (A : Type) (f : A -> nat) (P : A -> Type)
-      (F_sub : forall x : A, (forall (y : A | f y < f x), P y) -> P x),
-      forall x : A,
-        Fix_measure_sub A f P F_sub x =
-          F_sub x (fun (y : A | f y < f x) => Fix_measure_sub A f P F_sub y).
-  Proof.
-    intros ; apply Fix_measure_eq ; auto.
-    intros.
-    assert(f0 = g).
-    extensionality y ; apply H.
-    rewrite H0 ; auto.
-  Qed.
   
-  (** Tactic to unfold once a definition based on [Fix_measure_sub]. *)
+  (** Tactic to unfold once a definition based on [Fix_sub]. *)
   
   Ltac unfold_sub f fargs := 
     set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; 
-      rewrite fix_sub_measure_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
+      rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig.
 
 End WfExtensionality.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9658f792e..4e5eded8e 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -330,7 +330,7 @@ let explain_hole_kind env evi = function
       str "the type of " ++ Nameops.pr_id id
   | BinderType Anonymous ->
       str "the type of this anonymous binder"
-  | ImplicitArg (c,(n,ido)) ->
+  | ImplicitArg (c,(n,ido),b) ->
       let id = Option.get ido in
       str "the implicit parameter " ++
       pr_id id ++ spc () ++ str "of" ++
diff --git a/toplevel/record.ml b/toplevel/record.ml
index fe478f080..d22735f1d 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -281,7 +281,7 @@ let implicits_of_context ctx =
       match name with 
       | Name n -> Some n
       | Anonymous -> None
-    in ExplByPos (i, explname), (true, true))
+    in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
 let typeclasses_db = "typeclass_instances"
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b146e0c50..5d886c07e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -767,7 +767,7 @@ let vernac_syntactic_definition lid =
 let vernac_declare_implicits local r = function
   | Some imps ->
       Impargs.declare_manual_implicits local (global_with_alias r) ~enriching:false
-	(List.map (fun (ex,b,f) -> ex, (b,f)) imps)
+	(List.map (fun (ex,b,f) -> ex, (b,true,f)) imps)
   | None -> 
       Impargs.declare_implicits local (global_with_alias r)