- Implementation of a new typeclasses eauto procedure based on success

  and failure continuations, allowing to do safe cuts correctly.
- Fix bug #2097 by suppressing useless nf_evars calls.
- Improve the proof search strategy used by rewrite for subrelations and
  fix some hints.
Up to 20% speed improvement in setoid-intensive files.


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

2 files changed, 343 insertions, 129 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 31ffc8897..3c3ff4984 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -46,6 +46,59 @@ let typeclasses_db = "typeclass_instances"
 let _ = Auto.auto_init := (fun () -> 
   Auto.create_hint_db false typeclasses_db full_transparent_state true)
 
+exception Found of evar_map
+
+let is_dependent ev evm = 
+  Evd.fold (fun ev' evi dep -> 
+    if ev = ev' then dep
+    else dep || occur_evar ev evi.evar_concl)
+    evm false
+
+let valid goals p res_sigma l = 
+  let evm = 
+    List.fold_left2 
+      (fun sigma (ev, evi) prf ->
+	let cstr, obls = Refiner.extract_open_proof !res_sigma prf in
+	  if not (Evd.is_defined sigma ev) then
+	    Evd.define ev cstr sigma
+	  else sigma)
+      !res_sigma goals l
+  in raise (Found evm)
+
+let evars_to_goals p evm =
+  let goals, evm' = 
+    Evd.fold
+      (fun ev evi (gls, evm') ->
+	if evi.evar_body = Evar_empty 
+	  && Typeclasses.is_resolvable evi
+	  (* 	  && not (is_dependent ev evm) *)
+	  && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else 
+	  (gls, Evd.add evm' ev evi))
+      evm ([], Evd.empty)
+  in
+    if goals = [] then None
+    else
+      let goals = List.rev goals in
+	Some (goals, evm')
+
+let run_with_evars_to_goals p cont evm =
+  match evars_to_goals p evm with
+  | None -> None
+  | Some (goals, evm') ->
+      let gls = { it = List.map snd goals; sigma = evm' } in
+      let res_sigma = ref evm' in
+      let gls', valid' = cont (gls, valid goals p res_sigma) in
+	res_sigma := Evarutil.nf_evars (sig_sig gls');
+	try ignore(valid' []); assert(false) 
+	with Found evm' -> 
+	  Some (Evarutil.nf_evar_defs (Evd.evars_reset_evd evm' evm))
+
+let solve_remaining_evars tac gl =
+  let res = run_with_evars_to_goals (fun ev evi -> Typeclasses.is_class_evar evi) tac (project gl) in
+    match res with
+    | None -> tclIDTAC gl
+    | Some res -> Refiner.tclEVARS res gl
+
 (** Typeclasses instance search tactic / eauto *)
 
 let intersects s t =
@@ -74,12 +127,23 @@ let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
     Clenvtac.clenv_refine true ~with_classes:false clenv' gls
-      
+
 let unify_resolve flags (c,clenv) gls = 
   let clenv' = connect_clenv gls clenv in
   let clenv' = clenv_unique_resolver false ~flags clenv' gls in
     Clenvtac.clenv_refine false ~with_classes:false clenv' gls
 
+(** Hack to properly solve dependent evars that are typeclasses *)
+
+let forward_typeclasses_eauto = ref (fun gl -> failwith "Undefined forward_typeclasses_eauto")
+let typeclasses_evars gl = solve_remaining_evars !forward_typeclasses_eauto gl
+
+let unify_e_resolve flags (c,clenv) =
+  unify_e_resolve flags (c, clenv)
+
+let unify_resolve flags (c,clenv) =
+  unify_resolve flags (c, clenv)
+
 let flags_of_state st =
   {auto_unif_flags with 
     modulo_conv_on_closed_terms = Some st; modulo_delta = st}
@@ -171,7 +235,15 @@ let is_dep gl gls =
 	    let evs' = Evarutil.evars_of_term gl.evar_concl in
 	      intersects evs evs')
 	false gls
-	
+
+let is_ground gl = 
+  Evarutil.is_ground_term (project gl) (pf_concl gl)
+
+let nb_empty_evars s = 
+  Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
+
+let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
+
 module SearchProblem = struct
     
   type state = search_state
@@ -179,8 +251,6 @@ module SearchProblem = struct
   let debug = ref false
 
   let success s = sig_it (fst s.tacres) = []
-
-  let pr_ev evs ev = Printer.pr_constr_env (Evd.evar_env ev) (Evarutil.nf_evar evs ev.Evd.evar_concl)
     
   let pr_goals gls =
     let evars = Evarutil.nf_evars (Refiner.project gls) in
@@ -199,8 +269,6 @@ module SearchProblem = struct
 	  with e when catchable e -> aux tacl
     in aux l
       
-  let nb_empty_evars s = 
-    Evd.fold (fun ev evi acc -> if evi.evar_body = Evar_empty then succ acc else acc) s 0
 
   (* Ordering of states is lexicographic on depth (greatest first) then
      priority (lowest pri means higher priority), then number of remaining goals. *)
@@ -220,35 +288,33 @@ module SearchProblem = struct
       []
     else      
       let (cut, do_cut, ldb as hdldb) = List.hd s.localdb in
+	Option.iter (fun r -> r := true) do_cut;
 	if !cut then
 (* 	  let {it=gls; sigma=sigma} = fst s.tacres in *)
 (* 	    msg (str"cut:" ++ pr_ev sigma (List.hd gls) ++ str"\n"); *)
 	    []
-	else begin
-	  let {it=gl; sigma=sigma} = fst s.tacres in 
-	    Option.iter (fun r ->
-(*  	      msg (str"do cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
-	      r := true) do_cut;
-(* 	  let sigma = Evarutil.nf_evars sigma in *)
-	  let gl = List.map (Evarutil.nf_evar_info sigma) gl in
-	  let nbgl = List.length gl in
-(* 	  let gl' = { it = gl ; sigma = sigma } in *)
-(* 	  let tacres' = gl', snd s.tacres in *)
+	else
+	  begin
+	    let {it=gl; sigma=sigma} = fst s.tacres in 
+	    (* 	  let sigma = Evarutil.nf_evars sigma in *)
+(* 	    let gl = List.map (Evarutil.nf_evar_info sigma) gl in *)
+	    let nbgl = List.length gl in
+	      (* 	  let gl' = { it = gl ; sigma = sigma } in *)
+	      (* 	  let tacres' = gl', snd s.tacres in *)
 	  let new_db, localdb =
-	    let tl = List.tl s.localdb in hdldb, tl
-(* 	      match tl with *)
-(* 	      | [] -> hdldb, tl *)
-(* 	      | (cut', do', ldb') :: rest -> *)
-(* 		  if not (is_dep (List.hd gl) (List.tl gl)) then *)
-(* 		    let fresh = ref false in *)
-(* 		      if do' = None then ( *)
-(* (\*  			msg (str"adding a cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *\) *)
-(* 			(fresh, None, ldb), (cut', Some fresh, ldb') :: rest *)
-(* 		      ) else ( *)
-(* (\* 			msg (str"keeping the previous cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *\) *)
-(* 			(cut', None, ldb), tl ) *)
-(* 		  else hdldb, tl *)
-	  in let localdb = new_db :: localdb in
+	    let tl = List.tl s.localdb in
+	      match tl with
+	      | [] -> hdldb, tl
+	      | (cut', do', ldb') :: rest ->
+		  if Evarutil.is_ground_term sigma (List.hd gl).evar_concl (* not (is_dep (List.hd gl) (List.tl gl)) *) then
+		    let fresh = ref false in
+ 		      ((* msg (str"adding a cut:" ++ pr_ev sigma (List.hd gl) ++ str"\n"); *)
+		       (fresh, do', ldb), (cut', Some fresh, ldb') :: rest)
+		  else (
+ 		    msg (str"not ground:" ++ pr_ev sigma (List.hd gl) ++ str"\n");
+		    hdldb, tl)
+	  in 
+	  let localdb = new_db :: localdb in
 	  let intro_tac =
 	    List.map
 	      (fun ((lgls,_) as res,pri,pp) ->
@@ -282,14 +348,130 @@ module SearchProblem = struct
 	      List.map possible_resolve l
 	  in
 	    List.sort compare (intro_tac @ rec_tacs)
-	end
-	  
+	  end
+	    
   let pp s = 
     msg (hov 0 (str " depth=" ++ int s.depth ++ spc () ++ 
 		  s.last_tactic ++ str "\n"))
 
 end
 
+type validation = evar_map -> proof_tree list -> proof_tree
+
+type autoinfo = { hints : Auto.hint_db; auto_depth: int; auto_last_tac: std_ppcmds }
+type autogoal = goal * autoinfo
+type 'ans fk = unit -> 'ans
+type ('a,'ans) sk = 'a -> 'ans fk -> 'ans
+type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans }
+  
+type auto_result = autogoal list sigma * validation
+
+type atac = auto_result tac
+  
+let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
+  { skft = fun sk fk {it = gl,hints; sigma=s} ->
+    let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
+      match res with
+      | Some (gls,v) -> sk (f gls hints, fun _ -> v) fk
+      | None -> fk () }
+    
+let intro_tac : atac = 
+  lift_tactic Tactics.intro 
+    (fun {it = gls; sigma = s} info ->
+      let gls' =
+	List.map (fun g' ->
+	  let env = evar_env g' in
+	  let hint = make_resolve_hyp env s (List.hd (evar_context g')) in
+	  let ldb = Hint_db.add_list hint info.hints in
+	    (g', { info with hints = ldb; auto_last_tac = str"intro" })) gls
+      in {it = gls'; sigma = s})
+
+let id_tac : atac = 
+  { skft = fun sk fk {it = gl; sigma = s} -> 
+    sk ({it = [gl]; sigma = s}, fun _ pfs -> List.hd pfs) fk }
+
+(* Ordering of states is lexicographic on the number of remaining goals. *)
+let compare (pri, _, (res, _)) (pri', _, (res', _)) =
+  let nbgoals s =
+    List.length (sig_it s) + nb_empty_evars (sig_sig s)
+  in
+  let pri = pri - pri' in
+    if pri <> 0 then pri
+    else nbgoals res - nbgoals res'
+
+let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = 
+  { skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
+
+let solve_tac (x : 'a tac) : 'a tac =
+  { skft = fun sk fk gls -> x.skft (fun ({it = gls},_ as res) fk -> if gls = [] then sk res fk else fk ()) fk gls }
+      
+let hints_tac hints = 
+  { skft = fun sk fk {it = gl,info; sigma = s} ->
+    if !SearchProblem.debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ info.auto_last_tac
+					 ++ spc () ++ str "->" ++ spc () ++ pr_ev s gl);
+    let possible_resolve ((lgls,v) as res, pri, pp) =
+      (pri, pp, res)
+    in
+    let tacs =
+      let poss = e_possible_resolve hints info.hints gl.evar_concl in
+      let l =
+	Util.list_map_append (fun (tac, pri, pptac) ->
+	  try [tac {it = gl; sigma = s}, pri, pptac] with e when catchable e -> [])
+	  poss
+      in
+	List.map possible_resolve l
+    in
+    let tacs = List.sort compare tacs in
+    let info = { info with auto_depth = succ info.auto_depth } in
+    let rec aux = function
+      | (_, pp, ({it = gls; sigma = s}, v)) :: tl ->
+	  if !SearchProblem.debug then msgnl (str"depth=" ++ int info.auto_depth ++ str": " ++ pp
+					       ++ spc () ++ str"succeeded on" ++ spc () ++ pr_ev s gl);
+	  let fk =
+	    (fun () -> if !SearchProblem.debug then msgnl (str"backtracked after " ++ pp ++ spc () ++ str"failed");
+	    aux tl) 
+	  in
+	  let glsv = {it = List.map (fun g -> g, { info with auto_last_tac = pp }) gls; sigma = s}, fun _ -> v in
+	    sk glsv fk
+      | [] -> fk ()
+    in aux tacs }
+    
+let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
+  let rec aux s (acc : (autogoal list * validation) list) fk = function
+    | (gl,info) :: gls ->
+	second.skft (fun ({it=gls';sigma=s'},v') fk' -> 
+	  let fk'' = if gls' = [] && Evarutil.is_ground_term s gl.evar_concl then 
+	    (if !SearchProblem.debug then msgnl (str"no backtrack on" ++ pr_ev s gl); fk) else fk' in
+	    aux s' ((gls',v')::acc) fk'' gls) fk {it = (gl,info); sigma = s}
+    | [] -> Some (List.rev acc, s, fk)
+  in fun ({it = gls; sigma = s},v) fk -> 
+    let rec aux' = function
+      | None -> fk ()
+      | Some (res, s', fk') ->
+	  let goals' = List.concat (List.map (fun (gls,v) -> gls) res) in
+	  let v' s' pfs' : proof_tree =
+	    let (newpfs, rest) = List.fold_left (fun (newpfs,pfs') (gls,v) ->
+	      let before, after = list_split_at (List.length gls) pfs' in
+		(v s' before :: newpfs, after))
+	      ([], pfs') res
+	    in assert(rest = []); v s' (List.rev newpfs)
+	  in sk ({it = goals'; sigma = s'}, v') (fun () -> aux' (fk' ()))
+    in aux' (aux s [] (fun () -> None) gls)
+
+let then_tac (first : atac) (second : atac) : atac =
+  { skft = fun sk fk -> first.skft (then_list second sk) fk }
+  
+let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = 
+  t.skft (fun x _ -> Some x) (fun _ -> None) gl
+
+let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : auto_result option = 
+  (then_list t (fun x _ -> Some x)) 
+    (gl, fun s pfs -> valid goals p (ref s) pfs)
+    (fun _ -> None)
+    
+let rec fix (t : 'a tac) : 'a tac = 
+  then_tac t { skft = fun sk fk -> (fix t).skft sk fk }
+
 module Search = Explore.Make(SearchProblem)
 
 let make_initial_state n gls dblist localdbs =
@@ -303,8 +485,7 @@ let make_initial_state n gls dblist localdbs =
 let e_depth_search debug s =
   let tac = if debug then
     (SearchProblem.debug := true; Search.debug_depth_first) else Search.depth_first in
-  let s = tac s in
-    s.tacres
+  let s = tac s in s.tacres
 
 let e_breadth_search debug s =
   try
@@ -335,6 +516,44 @@ let make_resolve_hyp env sigma st flags pri (id, _, cty) =
 	[make_exact_entry pri; make_apply_entry env sigma flags pri]
     else []
 
+let make_autogoal ?(st=full_transparent_state) g =
+  let sign = pf_hyps g in
+  let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) None) sign in
+  let hints = Hint_db.add_list hintlist (Hint_db.empty st true) in
+    (g.it, { hints = hints ; auto_depth = 0; auto_last_tac = mt() })
+      
+let make_autogoals ?(st=full_transparent_state) gs evm' =
+  { it = List.map (fun g -> make_autogoal ~st {it = snd g; sigma = evm'}) gs; sigma = evm' }
+    
+let run_on_evars ?(st=full_transparent_state) p evm tac =
+  match evars_to_goals p evm with
+  | None -> raise Not_found
+  | Some (goals, evm') ->
+      match run_list_tac tac p goals (make_autogoals ~st goals evm') with
+      | None -> raise Not_found
+      | Some (gls, v) -> 
+	  try ignore(v (sig_sig gls) []); assert(false) 
+	  with Found evm' -> 
+	    Some (Evd.evars_reset_evd evm' evm)
+
+let eauto hints g =
+  let tac = fix (hints_tac hints) in
+  let gl = { it = make_autogoal g; sigma = project g } in
+    match run_tac tac gl with
+    | None -> raise Not_found
+    | Some ({it = goals; sigma = s}, valid) -> 
+	{it = List.map fst goals; sigma = s}, valid s
+
+let real_eauto st hints p evd =
+  let tac = fix (hints_tac hints) in
+    run_on_evars ~st p evd tac
+      
+TACTIC EXTEND ContEauto
+ | [ "conteauto" "with" ne_preident_list(l) ] -> [ fun gl ->
+     try eauto (List.map Auto.searchtable_map l) gl
+     with Not_found -> tclFAIL 0 (str" Continuation-based eauto failed") gl ]
+END
+
 let make_local_hint_db st eapply lems g =
   let sign = pf_hyps g in
   let hintlist = list_map_append (pf_apply make_resolve_hyp g st (eapply,false,false) None) sign in
@@ -366,44 +585,19 @@ let typeclasses_eauto debug n lems gls =
   let db = searchtable_map typeclasses_db in
     e_search_auto debug n lems (Hint_db.transparent_state db) [db] gls
 
-exception Found of evar_map
+let resolve_all_evars_once debug (mode, depth) p evd =
+  match run_with_evars_to_goals p (typeclasses_eauto debug (mode, depth) []) evd with
+  | None -> evd
+  | Some res -> res
 
-let valid goals p res_sigma l = 
-  let evm = 
-    List.fold_left2 
-      (fun sigma (ev, evi) prf ->
-	let cstr, obls = Refiner.extract_open_proof !res_sigma prf in
-	  if not (Evd.is_defined sigma ev) then
-	    Evd.define ev cstr sigma
-	  else sigma)
-      !res_sigma goals l
-  in raise (Found evm)
+let resolve_all_evars_once debug (mode, depth) p evd =
+  let db = searchtable_map typeclasses_db in
+    match real_eauto (Hint_db.transparent_state db) [db] p evd with
+    | None -> raise Not_found
+    | Some res -> res
 
-let is_dependent ev evm = 
-  Evd.fold (fun ev' evi dep -> 
-    if ev = ev' then dep
-    else dep || occur_evar ev evi.evar_concl)
-    evm false
-    
-let resolve_all_evars_once debug (mode, depth) env p evd =
-  let evm =  evd in
-  let goals, evm' = 
-    Evd.fold
-      (fun ev evi (gls, evm') ->
-	if evi.evar_body = Evar_empty 
-	  && Typeclasses.is_resolvable evi
-(* 	  && not (is_dependent ev evm) *)
-	  && p ev evi then ((ev,evi) :: gls, Evd.add evm' ev (Typeclasses.mark_unresolvable evi)) else 
-	  (gls, Evd.add evm' ev evi))
-      evm ([], Evd.empty)
-  in
-  let goals = List.rev goals in
-  let gls = { it = List.map snd goals; sigma = evm' } in
-  let res_sigma = ref evm' in
-  let gls', valid' = typeclasses_eauto debug (mode, depth) [] (gls, valid goals p res_sigma) in
-    res_sigma := Evarutil.nf_evars (sig_sig gls');
-    try ignore(valid' []); assert(false) 
-    with Found evm' -> Evarutil.nf_evar_defs (Evd.evars_reset_evd evm' evd)
+let _ = 
+  forward_typeclasses_eauto := (typeclasses_eauto false (true, default_eauto_depth) [])
 
 exception FoundTerm of constr
 
@@ -452,7 +646,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
   let rec aux n p evd =
     if has_undefined p oevm evd then
       if n > 0 then
-	let evd' = resolve_all_evars_once debug m env p evd in
+	let evd' = resolve_all_evars_once debug m p evd in
 	  aux (pred n) p evd'
       else None
     else Some evd
@@ -460,7 +654,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
   let rec docomp evd = function
     | [] -> evd
     | comp :: comps ->
-	let res = try aux 3 (p comp) evd with Not_found -> None in
+	let res = try aux 1 (p comp) evd with Not_found -> None in
 	  match res with
 	  | None -> 
 	      if fail then 
@@ -542,6 +736,7 @@ END
       
 VERNAC COMMAND EXTEND Typeclasses_Settings
  | [ "Typeclasses" "eauto" ":=" debug(d) search_mode(s) depth(depth) ] -> [ 
+     SearchProblem.debug := d;
      let mode = match s with Some t -> t | None -> true in
      let depth = match depth with Some i -> i | None -> default_eauto_depth in
        Typeclasses.solve_instanciations_problem :=
@@ -667,4 +862,13 @@ TACTIC EXTEND varify
   ]
 END
 
+TACTIC EXTEND not_evar
+  [ "not_evar" constr(ty) ] -> [ 
+    match kind_of_term ty with
+    | Evar _ -> tclFAIL 0 (str"Evar")
+    | _ -> tclIDTAC ]
+END
+
+
+
 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 5f19d08de..216beab54 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -112,6 +112,8 @@ let default_relation = lazy (gen_constant ["Classes"; "SetoidTactics"] "DefaultR
 
 let subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "subrelation")
 let is_subrelation = lazy (gen_constant ["Classes"; "RelationClasses"] "is_subrelation")
+let do_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "do_subrelation")
+let apply_subrelation = lazy (gen_constant ["Classes"; "Morphisms"] "apply_subrelation")
 
 let coq_relation = lazy (gen_constant ["Relations";"Relation_Definitions"] "relation")
 let mk_relation a = mkApp (Lazy.force coq_relation, [| a |])
@@ -160,50 +162,49 @@ let split_head = function
     hd :: tl -> hd, tl
   | [] -> assert(false)
 
-let build_signature isevars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) =
-  let new_evar isevars env t =
-    Evarutil.e_new_evar isevars env
+let build_signature evars env m (cstrs : 'a option list) (finalcstr : 'a Lazy.t option) (f : 'a -> constr) =
+  let new_evar evars env t =
+    Evarutil.new_evar evars env
       (* ~src:(dummy_loc, ImplicitArg (ConstRef (Lazy.force respectful), (n, Some na))) *) t
   in
-  let mk_relty ty obj =
+  let mk_relty evars ty obj =
     match obj with
       | None -> 
 	  let relty = mk_relation ty in
-	    new_evar isevars env relty
-      | Some x -> f x
+	    new_evar evars env relty
+      | Some x -> evars, f x
   in
-  let rec aux env ty l =
-    let t = Reductionops.whd_betadeltaiota env ( !isevars) ty in
+  let rec aux env evars ty l =
+    let t = Reductionops.whd_betadeltaiota env evars ty in
       match kind_of_term t, l with
       | Prod (na, ty, b), obj :: cstrs -> 
 	  if dependent (mkRel 1) b then
-	    let (b, arg, evars) = aux (Environ.push_rel (na, None, ty) env) b cstrs in
-	    let ty = Reductionops.nf_betaiota ( !isevars) ty in
+	    let (evars, b, arg, cstrs) = aux (Environ.push_rel (na, None, ty) env) evars b cstrs in
+	    let ty = Reductionops.nf_betaiota evars ty in
 	    let pred = mkLambda (na, ty, b) in
 	    let liftarg = mkLambda (na, ty, arg) in
 	    let arg' = mkApp (Lazy.force forall_relation, [| ty ; pred ; liftarg |]) in
-	      mkProd(na, ty, b), arg', (ty, None) :: evars
+	      evars, mkProd(na, ty, b), arg', (ty, None) :: cstrs
 	  else
-	    let (b', arg, evars) = aux env (subst1 mkProp b) cstrs in
-	    let ty = Reductionops.nf_betaiota( !isevars) ty in
-	    let relty = mk_relty ty obj in
+	    let (evars, b', arg, cstrs) = aux env evars (subst1 mkProp b) cstrs in
+	    let ty = Reductionops.nf_betaiota evars ty in
+	    let evars, relty = mk_relty evars ty obj in
 	    let newarg = mkApp (Lazy.force respectful, [| ty ; b' ; relty ; arg |]) in
-	      mkProd(na, ty, b), newarg, (ty, Some relty) :: evars
+	      evars, mkProd(na, ty, b), newarg, (ty, Some relty) :: cstrs
       | _, obj :: _ -> anomaly "build_signature: not enough products"
       | _, [] -> 
 	  (match finalcstr with
 	      None -> 
-		let t = Reductionops.nf_betaiota( !isevars) ty in
-		let rel = mk_relty t None in 
-		  t, rel, [t, Some rel]
+		let t = Reductionops.nf_betaiota evars ty in
+		let evars, rel = mk_relty evars t None in 
+		  evars, t, rel, [t, Some rel]
 	    | Some codom -> let (t, rel) = Lazy.force codom in
-			      t, rel, [t, Some rel])
-  in aux env m cstrs
-
+			      evars, t, rel, [t, Some rel])
+  in aux env evars m cstrs
+    
 let proper_proof env evars carrier relation x =
-  let goal =
-    mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |])
-  in Evarutil.e_new_evar evars env goal
+  let goal = mkApp (Lazy.force proper_proxy_type, [| carrier ; relation; x |])
+  in Evarutil.new_evar evars env goal
 
 let find_class_proof proof_type proof_method env evars carrier relation =
   try 
@@ -410,53 +411,63 @@ type rewrite_result = rewrite_result_info option
   
 type strategy = Environ.env -> evar_defs -> constr -> types ->
   constr option -> evar_defs -> rewrite_result option
+  
+let resolve_subrelation env sigma car rel rel' res =
+  if eq_constr rel rel' then res
+  else
+(*   try let evd' = Evarconv.the_conv_x env rel rel' res.rew_evars in *)
+(* 	{ res with rew_evars = evd' } *)
+(*   with NotConvertible -> *)
+    let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
+    let evars, subrel = Evarutil.new_evar res.rew_evars env app in
+      { res with 
+	rew_prf = mkApp (subrel, [| res.rew_from ; res.rew_to ; res.rew_prf |]);
+	rew_rel = rel';
+	rew_evars = evars }
+
 
 let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars =
-  let morph_instance, proj, sigargs, m', args, args' = 
+  let evars, morph_instance, proj, sigargs, m', args, args' = 
     let first = try (array_find args' (fun i b -> b <> None)) with Not_found -> raise (Invalid_argument "resolve_morphism") in
     let morphargs, morphobjs = array_chop first args in
     let morphargs', morphobjs' = array_chop first args' in
     let appm = mkApp(m, morphargs) in
     let appmtype = Typing.type_of env sigma appm in
-    let cstrs = List.map (function None -> None | Some r -> Some (r.rew_car, r.rew_rel)) (Array.to_list morphobjs') in
-    let appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a,r) -> r) in
+    let cstrs = List.map (Option.map (fun r -> r.rew_car, r.rew_rel)) (Array.to_list morphobjs') in
+      (* Desired signature *)
+    let evars, appmtype', signature, sigargs = build_signature evars env appmtype cstrs cstr (fun (a,r) -> r) in
+      (* Actual signature found *)
     let cl_args = [| appmtype' ; signature ; appm |] in
     let app = mkApp (Lazy.force proper_type, cl_args) in
-    let morph = Evarutil.e_new_evar evars env app in
-      morph, morph, sigargs, appm, morphobjs, morphobjs'
+    let env' = Environ.push_named
+      (id_of_string "do_subrelation", Some (Lazy.force do_subrelation), Lazy.force apply_subrelation)
+      env
+    in
+    let evars, morph = Evarutil.new_evar evars env' app in
+      evars, morph, morph, sigargs, appm, morphobjs, morphobjs'
   in 
-  let projargs, respars, typeargs = 
+  let projargs, evars, respars, typeargs = 
     array_fold_left2 
-      (fun (acc, sigargs, typeargs') x y -> 
+      (fun (acc, evars, sigargs, typeargs') x y -> 
 	let (carrier, relation), sigargs = split_head sigargs in
 	  match relation with
 	  | Some relation ->
 	      (match y with
 	      | None ->
-		  let proof = proper_proof env evars carrier relation x in
-		    [ proof ; x ; x ] @ acc, sigargs, x :: typeargs'
+		  let evars, proof = proper_proof env evars carrier relation x in
+		    [ proof ; x ; x ] @ acc, evars, sigargs, x :: typeargs'
 	      | Some r -> 
-		  [ r.rew_prf; r.rew_to; x ] @ acc, sigargs, r.rew_to :: typeargs')
+		  [ r.rew_prf; r.rew_to; x ] @ acc, evars, sigargs, r.rew_to :: typeargs')
 	  | None -> 
 	      if y <> None then error "Cannot rewrite the argument of a dependent function";
-	      x :: acc, sigargs, x :: typeargs')
-      ([], sigargs, []) args args'
+	      x :: acc, evars, sigargs, x :: typeargs')
+      ([], evars, sigargs, []) args args'
   in
   let proof = applistc proj (List.rev projargs) in
   let newt = applistc m' (List.rev typeargs) in
     match respars with
-	[ a, Some r ] -> (proof, (a, r, oldt, fnewt newt))
+	[ a, Some r ] -> evars, proof, a, r, oldt, fnewt newt
       | _ -> assert(false)
-  
-let resolve_subrelation env sigma car rel rel' res =
-  if convertible env sigma rel rel' then res
-  else
-    let app = mkApp (Lazy.force subrelation, [|car; rel; rel'|]) in
-    let evars, subrel = Evarutil.new_evar res.rew_evars env app in
-      { res with 
-	rew_prf = mkApp (subrel, [| res.rew_from ; res.rew_to ; res.rew_prf |]);
-	rew_rel = rel';
-	rew_evars = evars }
 	
 let apply_constraint env sigma car rel cstr res =
   match cstr with
@@ -505,7 +516,7 @@ let subterm all flags (s : strategy) : strategy =
 		  else 
 		    let res = s env sigma arg (Typing.type_of env sigma arg) None evars in
 		      match res with 
-		      | Some None -> (None :: acc, evars, Some false)
+		      | Some None -> (None :: acc, evars, if progress = None then Some false else progress)
 		      | Some (Some r) -> (Some r :: acc, r.rew_evars, Some true)
 		      | None -> (None :: acc, evars, progress))
 		([], evars, success) args
@@ -515,10 +526,9 @@ let subterm all flags (s : strategy) : strategy =
 	      | Some false -> Some None
 	      | Some true ->
 		  let args' = Array.of_list (List.rev args') in
-		  let evarsref = ref evars' in
-		  let (prf, (car, rel, c1, c2)) = resolve_morphism env sigma t m args args' cstr' evarsref in
+		  let evars', prf, car, rel, c1, c2 = resolve_morphism env sigma t m args args' cstr' evars' in
 		  let res = { rew_car = ty; rew_rel = rel; rew_from = c1;
-			      rew_to = c2; rew_prf = prf; rew_evars = !evarsref } in
+			      rew_to = c2; rew_prf = prf; rew_evars = evars' } in
 		    Some (Some res)
 	  in 
 	    if flags.on_morphisms then
@@ -1113,14 +1123,15 @@ let build_morphism_signature m =
 	| _ -> []
     in aux t
   in
-  let t', sig_, evars = build_signature isevars env t cstrs None snd in
+  let evars, t', sig_, cstrs = build_signature !isevars env t cstrs None snd in
+  let _ = isevars := evars in
   let _ = List.iter
     (fun (ty, rel) -> 
       Option.iter (fun rel ->
 	let default = mkApp (Lazy.force default_relation, [| ty; rel |]) in
 	  ignore (Evarutil.e_new_evar isevars env default)) 
 	rel)
-    evars
+    cstrs
   in
   let morph = 
     mkApp (Lazy.force proper_type, [| t; sig_; m |])
@@ -1132,15 +1143,14 @@ let build_morphism_signature m =
 	
 let default_morphism sign m =
   let env = Global.env () in
-  let isevars = ref Evd.empty in
   let t = Typing.type_of env Evd.empty m in
-  let _, sign, evars =
-    build_signature isevars env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
+  let evars, _, sign, cstrs =
+    build_signature Evd.empty env t (fst sign) (snd sign) (fun (ty, rel) -> rel)
   in
   let morph =
     mkApp (Lazy.force proper_type, [| t; sign; m |])
   in
-  let mor = resolve_one_typeclass env !isevars morph in
+  let mor = resolve_one_typeclass env evars morph in
     mor, proper_projection mor morph
     	  
 let add_setoid binders a aeq t n =