diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-10-20 14:36:38 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-10-20 14:36:38 +0000 |
| commit | d78039a61ec14b0aae127bd7d823e17bb3fea8f6 (patch) | |
| tree | 672fba5fbe9321a64422b73007aa9f030b0a0464 /proofs/logic.mli | |
| parent | 264afb325ec8e34009cf267d418ff0ba3ceb1da5 (diff) | |
module Clenv (debut)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@111 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/logic.mli')
| -rw-r--r-- | proofs/logic.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/proofs/logic.mli b/proofs/logic.mli index cbab2a90c..cbd94b52b 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -2,6 +2,7 @@ (* $Id$ *) (*i*) +open Names open Term open Sign open Evd @@ -9,6 +10,8 @@ open Environ open Proof_trees (*i*) +(* The primitive refiner. *) + val prim_refiner : prim_rule -> 'a evar_map -> goal -> goal list val prim_extractor : @@ -16,3 +19,14 @@ val prim_extractor : (typed_type, constr) env -> proof_tree -> constr val extract_constr : constr assumptions -> constr -> constr + + +(*s Refiner errors. *) + +type refiner_error = + | BadType of constr * constr * constr + | OccurMeta of constr + | CannotApply of constr * constr + | CannotUnify of constr * constr + +val error_cannot_unify : path_kind -> constr * constr -> 'a |