diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 22:21:33 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 22:21:33 +0000 |
| commit | 981ece2836d6366f3dad790c21350feb24b036af (patch) | |
| tree | c3045de235e39a7d5e9a90d291b643c03e601ab4 /pretyping/termops.ml | |
| parent | d5b1c83d0f0a60f9658c45ae902035f2fdef0c41 (diff) | |
Added full pattern-unification on Meta for tactic unification.
No way to control it yet; maybe flag use_evars_pattern_unification
should be generalized for that purpose.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14199 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index cd848984d..dfc1e2f89 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -282,6 +282,16 @@ let decompose_app_vect c = | App (f,cl) -> (f, cl) | _ -> (c,[||]) +let adjust_app_list_size f1 l1 f2 l2 = + let len1 = List.length l1 and len2 = List.length l2 in + if len1 = len2 then (f1,l1,f2,l2) + else if len1 < len2 then + let extras,restl2 = list_chop (len2-len1) l2 in + (f1, l1, applist (f2,extras), restl2) + else + let extras,restl1 = list_chop (len1-len2) l1 in + (applist (f1,extras), restl1, f2, l2) + (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name list) which is processed by [g na] (which typically cons [na] to |