diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-25 19:44:31 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-25 19:44:31 +0000 |
| commit | cb134451453a608cc486c1235fde2e08b7eab254 (patch) | |
| tree | f3b607367167c00f2834c753899527a034d0ae25 /contrib/first-order/formula.mli | |
| parent | ea484db49c183ab900a78204e4bb7ec233578bff (diff) | |
Ground and CCsolve updates
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4075 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/formula.mli')
| -rw-r--r-- | contrib/first-order/formula.mli | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index 89bd6d25f..3bcf1af0e 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -26,7 +26,7 @@ type kind_of_formula= Arrow of constr*constr |And of inductive*constr list |Or of inductive*constr list - |Exists of inductive*constr*constr*constr + |Exists of inductive*constr list |Forall of constr*constr |Atom of constr |Evaluable of Names.evaluable_global_reference * Term.constr @@ -36,9 +36,7 @@ type counter = bool -> metavariable val construct_nhyps : inductive -> int array -exception Dependent_Inductive - -val ind_hyps : inductive -> constr list -> Sign.rel_context array +val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array val kind_of_formula : constr -> kind_of_formula @@ -63,7 +61,7 @@ type left_arrow_pattern= | LLand of inductive*constr list | LLor of inductive*constr list | LLforall of constr - | LLexists of inductive*constr*constr*constr + | LLexists of inductive*constr list | LLarrow of constr*constr*constr | LLevaluable of Names.evaluable_global_reference @@ -82,6 +80,8 @@ type left_formula={id:global_reference; atoms:(bool*constr) list; internal:bool} +exception Is_atom of constr + val build_left_entry : global_reference -> types -> bool -> Proof_type.goal Tacmach.sigma -> counter -> (left_formula,types) sum |