diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 20:21:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-09-19 20:21:02 +0000 |
| commit | f34625ec7bbd0b2b6e2ce02a978d089b47c152ba (patch) | |
| tree | cde02214b20cfa015d3f936d91364a82b2a37990 | |
| parent | ae57ebb1a4d46c8c955940ac1b4c747a6bedcec6 (diff) | |
Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we
revert the catch of anomalies in reductionops.ml now (commit 13353)?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 b253b2375..b9cea418d 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 000000000..b0974a3fd --- /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. + |