From 981ece2836d6366f3dad790c21350feb24b036af Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 13 Jun 2011 22:21:33 +0000 Subject: 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 --- pretyping/termops.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'pretyping/termops.ml') 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 -- cgit v1.2.3