diff options
| author |  corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-08 15:18:22 +0000 |
|---|---|---|
| committer | corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-07-08 15:18:22 +0000 |
| commit | 67677229a29a049c8b1e8d8a4618d81b16730316 (patch) | |
| tree | c027a2dbfcf58c76c4f7e13a4efda7e47d071552 /contrib/first-order/formula.mli | |
| parent | e27e7e21f2fba8e20484a9f85c496f246f4c4753 (diff) | |
Ground update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4227 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/formula.mli')
| -rw-r--r-- | contrib/first-order/formula.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/contrib/first-order/formula.mli b/contrib/first-order/formula.mli index 140358523..9e027e240 100644 --- a/contrib/first-order/formula.mli +++ b/contrib/first-order/formula.mli @@ -14,6 +14,8 @@ open Libnames val qflag : bool ref +val red_flags: Closure.RedFlags.reds ref + val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) -> 'a -> 'a -> 'b -> 'b -> int @@ -28,9 +30,6 @@ val construct_nhyps : inductive -> int array val ind_hyps : int -> inductive -> constr list -> Sign.rel_context array -val match_with_evaluable : Proof_type.goal Tacmach.sigma -> - constr -> (evaluable_global_reference * constr) option - type atoms = {positive:constr list;negative:constr list} type side = Hyp | Concl | Hint |