diff options
| author | herbelin | 2010-09-24 22:23:02 +0000 |
|---|---|---|
| committer | herbelin | 2010-09-24 22:23:02 +0000 |
| commit | b676f7c47b39838611f4125dd1488b10f05aaaa1 (patch) | |
| tree | 5596a7c3f84493bbe2d10f0e23dc26868117a863 | |
| parent | 98b7bcfdbec5e34a8f3a1adaa141802fda4bf434 (diff) | |
Solving bug #2212 (unification under tuples now not allowed for
flexible types what seems a reasonable strategy).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13464 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3876c6b350..c96024553f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -843,13 +843,18 @@ type conjunction_status = | DefinedRecord of constant option list | NotADefinedRecordUseScheme of constr -let make_projection params cstr sign elim i n c = +let make_projection sigma params cstr sign elim i n c = let elim = match elim with | NotADefinedRecordUseScheme elim -> let (na,b,t) = List.nth cstr.cs_args i in let b = match b with None -> mkRel (i+1) | Some b -> b in let branch = it_mkLambda_or_LetIn b cstr.cs_args in - if noccur_between 1 (n-i-1) t then + if + (* excludes dependent projection types *) + noccur_between 1 (n-i-1) t + (* excludes flexible projection types *) + && not (isEvar (fst (whd_betaiota_stack sigma t))) + then let t = lift (i+1-n) t in Some (beta_applist (elim,params@[t;branch]),t) else @@ -884,7 +889,7 @@ let descend_in_conjunctions tac exit c gl = NotADefinedRecordUseScheme elim in tclFIRST (list_tabulate (fun i gl -> - match make_projection params cstr sign elim i n c with + match make_projection (project gl) params cstr sign elim i n c with | None -> tclFAIL 0 (mt()) gl | Some (p,pt) -> tclTHENS |