diff options
| -rw-r--r-- | tactics/tactics.ml | 3 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2360.v | 13 |
2 files changed, 15 insertions, 1 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b253b2375e..b9cea418d8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -884,7 +884,8 @@ let make_projection params cstr sign elim i n c = match List.nth l i with | Some proj -> let t = Typeops.type_of_constant (Global.env()) proj in - Some (beta_applist (mkConst proj,params),prod_applist t (params@[c])) + let args = extended_rel_vect 0 sign in + Some (beta_applist (mkConst proj,params),prod_applist t (params@[mkApp (c,args)])) | None -> None in Option.map (fun (abselim,elimt) -> let c = beta_applist (abselim,[mkApp (c,extended_rel_vect 0 sign)]) in diff --git a/test-suite/bugs/closed/shouldsucceed/2360.v b/test-suite/bugs/closed/shouldsucceed/2360.v new file mode 100644 index 0000000000..b0974a3fdd --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2360.v @@ -0,0 +1,13 @@ +(* This failed in V8.3 because descend_in_conjunctions built ill-typed terms *) +Definition interp (etyp : nat -> Type) (p: nat) := etyp p. + +Record Value (etyp : nat -> Type) := Mk { + typ : nat; + value : interp etyp typ +}. + +Definition some_value (etyp : nat -> Type) : (Value etyp). +Proof. + intros. + apply Mk. + |