- let diff = diff_term Stdpp.dummy_loc thing' newast in
- let status = add_to_interpr status diff
- in
- metasenv, subst, status, cic
+ match choices with
+ | [newast, metasenv, subst, cic] ->
+ let diff = diff_term Stdpp.dummy_loc thing' newast in
+ let status = add_to_interpr status diff
+ in
+ metasenv, subst, status, cic
+ | [] -> assert false
+ | _ ->
+ let diffs =
+ List.map (fun (ast,_,_,_) ->
+ diff_term Stdpp.dummy_loc thing' ast) choices
+ in
+ raise (Ambiguous_input (find_diffs diffs))