← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to toplevel/indschemes.ml

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
toplevel/indschemes.ml
1
1
(************************************************************************)
2
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
3
 
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 
3
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
4
4
(*   \VV/  **************************************************************)
5
5
(*    //   *      This file is distributed under the terms of the       *)
6
6
(*         *       GNU Lesser General Public License Version 2.1        *)
7
7
(************************************************************************)
8
8
 
9
 
(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *)
 
9
(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
10
10
 
11
11
(* Created by Hugo Herbelin from contents related to inductive schemes
12
12
   initially developed by Christine Paulin (induction schemes), Vincent
295
295
*)
296
296
  | (None,t)::q ->
297
297
      let l1,l2 = split_scheme q in
298
 
      let names inds recs x y z =
 
298
      let names inds recs isdep y z =
299
299
        let ind = smart_global_inductive y in
300
 
        let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
 
300
        let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
301
301
        let z' = family_of_sort (interp_sort z) in
302
302
        let suffix = (
303
303
          match sort_of_ind with
304
304
          | InProp ->
305
 
              if x then (match z' with
 
305
              if isdep then (match z' with
 
306
              | InProp -> inds ^ "_dep"
 
307
              | InSet  -> recs ^ "_dep"
 
308
              | InType -> recs ^ "t_dep")
 
309
              else ( match z' with
 
310
              | InProp -> inds
 
311
              | InSet -> recs
 
312
              | InType -> recs ^ "t" )
 
313
          | _ ->
 
314
              if isdep then (match z' with
 
315
              | InProp -> inds
 
316
              | InSet -> recs
 
317
              | InType -> recs ^ "t" )
 
318
              else (match z' with
306
319
              | InProp -> inds ^ "_nodep"
307
320
              | InSet -> recs ^ "_nodep"
308
321
              | InType -> recs ^ "t_nodep")
309
 
              else ( match z' with
310
 
              | InProp -> inds
311
 
              | InSet -> recs
312
 
              | InType -> recs ^ "t" )
313
 
          | _ ->
314
 
              if x then (match z' with
315
 
              | InProp -> inds
316
 
              | InSet -> recs
317
 
              | InType -> recs ^ "t" )
318
 
              else (match z' with
319
 
              | InProp -> inds ^ "_dep"
320
 
              | InSet  -> recs ^ "_dep"
321
 
              | InType -> recs ^ "t_dep")
322
322
        ) in
323
323
        let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
324
324
        let newref = (dummy_loc,newid) in
325
 
          ((newref,x,ind,z)::l1),l2
 
325
          ((newref,isdep,ind,z)::l1),l2
326
326
      in
327
327
        match t with
328
328
        | CaseScheme (x,y,z) -> names "_case" "_case" x y z