diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-30 15:06:48 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-30 15:06:48 +0000 |
| commit | f5f283ec29d79a64d8fdda92823fe606a475e625 (patch) | |
| tree | 9ce71088b933336bad04250d32e9271498576eb0 /contrib/correctness/past.mli | |
| parent | d7550d7625f9eb9bc9c0e88dabd744f6b1530891 (diff) | |
branchement extraction (bytecode seulement)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/correctness/past.mli')
| -rw-r--r-- | contrib/correctness/past.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli index 36022f208..d674f7d10 100644 --- a/contrib/correctness/past.mli +++ b/contrib/correctness/past.mli @@ -64,11 +64,11 @@ type cc_bind_type = | CC_typed_binder of cc_type | CC_untyped_binder type cc_binder = variable * cc_bind_type type cc_term = | CC_var of variable - | CC_letin of bool * cc_type * cc_binder list * (cc_term * Term.constr) * - cc_term + | CC_letin of + bool * cc_type * cc_binder list * (cc_term * Term.case_info) * cc_term | CC_lam of cc_binder list * cc_term | CC_app of cc_term * cc_term list | CC_tuple of bool * cc_type list * cc_term list - | CC_case of cc_type * (cc_term * Term.constr) * cc_term list + | CC_case of cc_type * (cc_term * Term.case_info) * cc_term list | CC_expr of Term.constr | CC_hole of cc_type |