diff options
author | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
tree | d7303613741c5796b58ced7db24ec7203327dbb2 /toplevel/indschemes.ml | |
parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'toplevel/indschemes.ml')
-rw-r--r-- | toplevel/indschemes.ml | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 9031d8a3..3596085f 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *) +(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Created by Hugo Herbelin from contents related to inductive schemes initially developed by Christine Paulin (induction schemes), Vincent @@ -295,34 +295,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 = Retyping.get_sort_family_of env Evd.empty (mkInd ind) 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 |