From 04133685b87ac84fae688744decf27ef935a1df6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 8 Nov 2011 15:30:44 +0000 Subject: Refined second_order_matching so that a constraint on which occurrences to abstract can be given. This allows to force "destruct" to necessarily abstract over all occurrences of its main argument (only the sub-arguments that occur in the inductive type of the main argument have their occurrences constrained by typing). This incidentally avoids "rewrite" succeeding in rewriting only a part of the occurrences it has to rewrite. This repairs the failure of RecursiveDefinition which failed after pattern unification fix from r14642). Full support for selecting occurrence of main argument still to be done though. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14648 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/evarconv.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/evarconv.mli') diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 27a71be24..3e2ca7aed 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -10,6 +10,7 @@ open Names open Term open Sign open Environ +open Termops open Reductionops open Evd @@ -43,4 +44,4 @@ val check_conv_record : constr * types list -> constr * types list -> val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit val second_order_matching : transparent_state -> env -> evar_map -> - existential -> constr -> evar_map * bool + existential -> occurrences option list -> constr -> evar_map * bool -- cgit v1.2.3