diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-08 15:30:44 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-08 15:30:44 +0000 |
| commit | 04133685b87ac84fae688744decf27ef935a1df6 (patch) | |
| tree | 8749e342e7c435ffe9a91e05a7a9cfd9057c569d /pretyping/evarconv.mli | |
| parent | 0cab74bb2906969e5ea72619be3a80dbc48b5675 (diff) | |
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
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 3 |
1 files changed, 2 insertions, 1 deletions
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 |