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
(************************************************************************)
9
(*i $Id: logic.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
20
(* This suppresses check done in [prim_refiner] for the tactic given in
21
argument; works by side-effect *)
23
val with_check : tactic -> tactic
25
(* [without_check] respectively means:\\
26
[Intro]: no check that the name does not exist\\
27
[Intro_after]: no check that the name does not exist and that variables in
28
its type does not escape their scope\\
29
[Intro_replacing]: no check that the name does not exist and that
30
variables in its type does not escape their scope\\
32
no check that the name exist and that its type is convertible\\
35
(* The primitive refiner. *)
37
val prim_refiner : prim_rule -> evar_map -> goal -> goal list * evar_map
42
(proof_variable list -> proof_tree -> constr)
43
-> proof_variable list -> proof_tree -> constr
45
val proof_variable_index : identifier -> proof_variable list -> int
47
(*s Refiner errors. *)
51
(*i Errors raised by the refiner i*)
52
| BadType of constr * constr * constr
53
| UnresolvedBindings of name list
54
| CannotApply of constr * constr
55
| NotWellTyped of constr
56
| NonLinearProof of constr
57
| MetaInType of constr
59
(*i Errors raised by the tactics i*)
61
| DoesNotOccurIn of constr * identifier
63
exception RefinerError of refiner_error
65
val catchable_exception : exn -> bool