diff options
| -rw-r--r-- | tactics/tactics.ml | 42 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 17 |
2 files changed, 47 insertions, 12 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index af81c7302..86f4eba43 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -863,18 +863,32 @@ let simplest_case c = general_case_analysis false (c,NoBindings) (* Apply a tactic below the products of the conclusion of a lemma *) +type conjunction_status = + | DefinedRecord of constant option list + | NotADefinedRecordUseScheme of constr + let make_projection params cstr sign elim i n c = - 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 - let t = lift (i+1-n) t in - let args = params@[t;branch;mkApp (c,extended_rel_vect 0 sign)] in - let p = it_mkLambda_or_LetIn (beta_applist (elim,args)) sign in - let pt = it_mkProd_or_LetIn t sign in - Some (p,pt) - else - None + 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 + let t = lift (i+1-n) t in + let args = params@[t;branch;mkApp (c,extended_rel_vect 0 sign)] in + let p = it_mkLambda_or_LetIn (beta_applist (elim,args)) sign in + let pt = it_mkProd_or_LetIn t sign in + Some (p,pt) + else + None + | DefinedRecord l -> + match List.nth l i with + | Some proj -> + let t = Typeops.type_of_constant (Global.env()) proj in + let args = params@[c] in + Some (applist (mkConst proj,args),prod_applist t args) + | None -> None + let descend_in_conjunctions tac exit c gl = try @@ -888,7 +902,11 @@ let descend_in_conjunctions tac exit c gl = let IndType (indf,_) = pf_apply find_rectype gl ccl in let params = snd (dest_ind_family indf) in let cstr = (get_constructors (pf_env gl) indf).(0) in - let elim = pf_apply build_case_analysis_scheme gl ind false sort in + let elim = + try DefinedRecord (Recordops.lookup_projections ind) + with Not_found -> + let elim = pf_apply build_case_analysis_scheme gl ind false sort in + NotADefinedRecordUseScheme elim in tclFIRST (list_tabulate (fun i gl -> match make_projection params cstr sign elim i n c with diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 3fc8a9792..cb55432fb 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -348,3 +348,20 @@ Goal True. eapply (fun (A:Prop) (x:A) => conj I x). exact I. Qed. + +(* The following was not accepted from r12612 to r12649 *) + +Record sig0 := { p1 : nat; p2 : p1 = 0 }. + +Goal forall x : sig0, p1 x = 0. +intro x; +apply x. +Qed. + +(* The following was accepted before r12612 but is still not accepted in r12650 + +Goal forall x : { x:nat | x = 0}, proj1_sig x = 0. +intro x; +apply x. + +*) |