is should behave like = on neutral terms

[gares]

elpi/src/builtin.ml

Lines 58 to 81 in 4d64e22

	(* Traverses the expression evaluating all custom evaluable functions *)
	let rec eval depth t =
	match look ~depth t with
	| Lam _ -> type_error "Evaluation of a lambda abstraction"
	| Builtin _ -> type_error "Evaluation of built-in predicate"
	| App (hd,arg,args) ->
	let f =
	try lookup_eval hd
	with Not_found ->
	function
	| [] -> assert false
	| x::xs -> mkApp hd (kool x) (List.map kool xs) in
	let args = List.map (fun x -> look ~depth (eval depth x)) (arg::args) in
	f args
	| UnifVar _ -> error "Evaluation of a non closed term (maybe delay)"
	| Const hd as x ->
	let f =
	try lookup_eval hd
	with Not_found -> fun _ -> kool x in
	f []
	| (Nil | Cons _ as x) ->
	type_error ("Lists cannot be evaluated: " ^ RawPp.Debug.show_term (kool x))
	| CData _ as x -> kool x
	;;

Indeed X is 2 works, but X is f _ fails, as well as X is x\x for no good reason.