diff options
| author | barras | 2004-02-18 18:32:33 +0000 |
|---|---|---|
| committer | barras | 2004-02-18 18:32:33 +0000 |
| commit | b5df1925bbc14f441247349b200aa3f5828e8427 (patch) | |
| tree | c158ac5d3d3133f2fce8188f3d0b4a75bd0c5415 /interp/topconstr.mli | |
| parent | 06900e469cd593c272f57c2af7d2e4f206a2f944 (diff) | |
- fixed the Assert_failure error in kernel/modops
- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
the CVS working dir)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/topconstr.mli')
| -rw-r--r-- | interp/topconstr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 65beaa511e..c6be360284 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -93,9 +93,9 @@ type constr_expr = (loc * cases_pattern_expr list * constr_expr) list | COrderedCase of loc * case_style * constr_expr option * constr_expr * constr_expr list - | CLetTuple of loc * name list * (name * constr_expr option) * + | CLetTuple of loc * name list * (name option * constr_expr option) * constr_expr * constr_expr - | CIf of loc * constr_expr * (name * constr_expr option) + | CIf of loc * constr_expr * (name option * constr_expr option) * constr_expr * constr_expr | CHole of loc | CPatVar of loc * (bool * patvar) |