From f5e644a53c69392f94eae01dd71ab79b4700a892 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 17 Feb 2013 14:56:11 +0000 Subject: A more informative message when the elimination predicate for destruct, rewrite, etc. is not well-typed. Also added support for a more informative message when the elimination predicate is not well-formed while using the smart "second-order" unification algorithm. However the "abstract_list_all" algorithm seems to remain more informative though, so we still use this algorithm for reporting about ill-typed predicates. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16207 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/evarconv.mli') diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index d3f8b451a..5a329f5f4 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -44,7 +44,7 @@ val check_conv_record : constr * types stack -> constr * types stack -> (constr stack * types stack) * constr * (int * constr) -val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit +val set_solve_evars : (env -> evar_map ref -> constr -> constr) -> unit val second_order_matching : transparent_state -> env -> evar_map -> existential -> occurrences option list -> constr -> evar_map * bool -- cgit v1.2.3