diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:07 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:07 +0000 |
commit | 5e6145c871eea1e94566b252b4bfc4cd752f42d5 (patch) | |
tree | 97dfa98357cb0cf90bf06c9d470e6788de84c3b1 /plugins/romega/refl_omega.ml | |
parent | 9b56e832ef591379dd1f2b29fe7d88513f7caf50 (diff) |
cList: set-as-list functions are now with an explicit comparison
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16920 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/romega/refl_omega.ml')
-rw-r--r-- | plugins/romega/refl_omega.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml index 635fc366f..752fa4598 100644 --- a/plugins/romega/refl_omega.ml +++ b/plugins/romega/refl_omega.ml @@ -921,7 +921,7 @@ let add_stated_equations env tree = let rec get_eclatement env = function i :: r -> let l = try (get_equation env i).e_depends with Not_found -> [] in - List.union (List.rev l) (get_eclatement env r) + List.union Pervasives.(=) (List.rev l) (get_eclatement env r) | [] -> [] let select_smaller l = @@ -1207,12 +1207,16 @@ let resolution env full_reified_goal systems_list = (* recupere explicitement ces equations *) let equations = List.map (get_equation env) useful_equa_id in let l_hyps' = List.uniquize (List.map (fun e -> e.e_origin.o_hyp) equations) in - let l_hyps = id_concl :: List.remove id_concl l_hyps' in + let l_hyps = id_concl :: List.remove Names.Id.equal id_concl l_hyps' in let useful_hyps = - List.map (fun id -> List.assoc id full_reified_goal) l_hyps in + List.map + (fun id -> List.assoc_f Names.Id.equal id full_reified_goal) l_hyps + in let useful_vars = let really_useful_vars = vars_of_equations equations in - let concl_vars = vars_of_prop (List.assoc id_concl full_reified_goal) in + let concl_vars = + vars_of_prop (List.assoc_f Names.Id.equal id_concl full_reified_goal) + in really_useful_vars @@ concl_vars in (* variables a introduire *) |