blob: 97f9acdb3ab173e2bc2d72b1eae38a7a517f58d6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Names
open Constr
val generate_functional_principle :
Evd.evar_map ref ->
(* do we accept interactive proving *)
bool ->
(* induction principle on rel *)
types ->
(* *)
Sorts.t array option ->
(* Name of the new principle *)
(Id.t) option ->
(* the compute functions to use *)
pconstant array ->
(* We prove the nth- principle *)
int ->
(* The tactic to use to make the proof w.r
the number of params
*)
(EConstr.constr array -> int -> Tacmach.tactic) ->
unit
exception No_graph_found
val make_scheme : Evd.evar_map ref ->
(pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit
val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit
|
