← Back to branch summary

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

« back to all changes in this revision

Viewing changes to pretyping/indrec.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
pretyping/indrec.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: indrec.mli 11562 2008-11-09 11:30:10Z herbelin $ i*)
 
10
 
 
11
(*i*)
 
12
open Names
 
13
open Term
 
14
open Declarations
 
15
open Inductiveops
 
16
open Environ
 
17
open Evd
 
18
(*i*)
 
19
 
 
20
(* Errors related to recursors building *)
 
21
 
 
22
type recursion_scheme_error =
 
23
  | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
 
24
  | NotMutualInScheme of inductive * inductive
 
25
 
 
26
exception RecursionSchemeError of recursion_scheme_error
 
27
 
 
28
(** Eliminations *)
 
29
 
 
30
(* These functions build elimination predicate for Case tactic *)
 
31
 
 
32
val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr
 
33
val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr
 
34
val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
 
35
 
 
36
(* This builds an elimination scheme associated (using the own arity
 
37
   of the inductive) *)
 
38
 
 
39
val build_indrec : env -> evar_map -> inductive -> constr
 
40
val instantiate_indrec_scheme : sorts -> int -> constr -> constr
 
41
val instantiate_type_indrec_scheme : sorts -> int -> constr -> types ->
 
42
  constr * types
 
43
 
 
44
(** Complex recursion schemes [Scheme] *)
 
45
 
 
46
val build_mutual_indrec : 
 
47
  env -> evar_map ->
 
48
    (inductive * mutual_inductive_body * one_inductive_body
 
49
    * bool * sorts_family) list
 
50
    -> constr list
 
51
 
 
52
(** Old Case/Match typing *)
 
53
 
 
54
val type_rec_branches : bool -> env -> evar_map -> inductive_type
 
55
  -> constr -> constr -> constr array * constr
 
56
val make_rec_branch_arg : 
 
57
  env -> evar_map ->
 
58
    int * ('b * constr) option array * int ->
 
59
    constr -> constructor_summary -> wf_paths list -> constr
 
60
 
 
61
(** Recursor names utilities *)
 
62
 
 
63
val lookup_eliminator : inductive -> sorts_family -> constr
 
64
val elimination_suffix : sorts_family -> string
 
65
val make_elimination_ident : identifier -> sorts_family -> identifier
 
66
 
 
67
 
 
68