diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-04-05 00:04:31 +0200 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-04-05 00:06:06 +0200 |
| commit | 4a8950ec7a0d9f2b216e67e69b446c064590a8e9 (patch) | |
| tree | 8ff3a916fad31fc2d405e8f3dcb783d0a1ae9e03 | |
| parent | 213251134eb56625e4b8cff2879d00cd8cc7ec6a (diff) | |
closing bug 3037
| -rw-r--r-- | plugins/funind/recdef.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ce731c1eb..614886073 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1180,7 +1180,8 @@ let build_and_l l = | App(_,_) -> let (f,_) = decompose_app t in eq_constr f (well_founded ()) - | _ -> assert false + | _ -> + false in let compare t1 t2 = let b1,b2= is_well_founded t1,is_well_founded t2 in @@ -1225,9 +1226,9 @@ let clear_goals = let build_new_goal_type () = let sub_gls_types = get_current_subgoals_types () in - (* Pp.msgnl (str "sub_gls_types1 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) + (* Pp.msgnl (str "sub_gls_types1 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let sub_gls_types = clear_goals sub_gls_types in - (* Pp.msgnl (str "sub_gls_types2 := " ++ Util.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) + (* Pp.msgnl (str "sub_gls_types2 := " ++ Pp.prlist_with_sep (fun () -> Pp.fnl () ++ Pp.fnl ()) Printer.pr_lconstr sub_gls_types); *) let res = build_and_l sub_gls_types in res |