diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 20:36:34 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-13 20:36:34 +0000 |
| commit | 463b54961c77aa7b5f21d2937628d9cc9cd5a06a (patch) | |
| tree | a28e2755c4f16865bde1d2ada4bf7b34711fd8ac | |
| parent | e56b4c209bf3c27f72f22457682aaaa83eb3c2e9 (diff) | |
Another bug of Scheme Induction (generated names dep/nodep were swapped).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14195 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | test-suite/success/Scheme.v | 1 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 20 |
2 files changed, 11 insertions, 10 deletions
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v index bde72c141..dd5aa81d1 100644 --- a/test-suite/success/Scheme.v +++ b/test-suite/success/Scheme.v @@ -1,3 +1,4 @@ (* This failed in 8.3pl2 *) Scheme Induction for eq Sort Prop. +Check eq_ind_dep. diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 901731530..489d28a4e 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -289,34 +289,34 @@ requested *) | (None,t)::q -> let l1,l2 = split_scheme q in - let names inds recs x y z = + let names inds recs isdep y z = let ind = smart_global_inductive y in let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in let z' = family_of_sort (interp_sort z) in let suffix = ( match sort_of_ind with | InProp -> - if x then (match z' with - | InProp -> inds ^ "_nodep" - | InSet -> recs ^ "_nodep" - | InType -> recs ^ "t_nodep") + if isdep then (match z' with + | InProp -> inds ^ "_dep" + | InSet -> recs ^ "_dep" + | InType -> recs ^ "t_dep") else ( match z' with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) | _ -> - if x then (match z' with + if isdep then (match z' with | InProp -> inds | InSet -> recs | InType -> recs ^ "t" ) else (match z' with - | InProp -> inds ^ "_dep" - | InSet -> recs ^ "_dep" - | InType -> recs ^ "t_dep") + | InProp -> inds ^ "_nodep" + | InSet -> recs ^ "_nodep" + | InType -> recs ^ "t_nodep") ) in let newid = add_suffix (basename_of_global (IndRef ind)) suffix in let newref = (dummy_loc,newid) in - ((newref,x,ind,z)::l1),l2 + ((newref,isdep,ind,z)::l1),l2 in match t with | CaseScheme (x,y,z) -> names "_case" "_case" x y z |