diff options
| author | barras | 2004-01-09 19:02:58 +0000 |
|---|---|---|
| committer | barras | 2004-01-09 19:02:58 +0000 |
| commit | b1bd8f2a50863a6ca77b6f05b3f1756648cfe936 (patch) | |
| tree | f9ab63c12f45c28bcc9320712e401c6ef32f26a1 /contrib/interface/vtp.ml | |
| parent | c4bc84f02c7d22402824514d70c6d5e66f511bfc (diff) | |
bugs avec Pose et Assert
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/vtp.ml')
| -rw-r--r-- | contrib/interface/vtp.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 5d7cff4cf5..9f8ece9b23 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -910,9 +910,12 @@ and fPROOF_SCRIPT = function (List.iter fCOMMAND l); fNODE "proof_script" (List.length l) and fRECCONSTR = function -| CT_coerce_CONSTR_to_RECCONSTR x -> fCONSTR x +| CT_coerce_CONSTR_to_RECCONSTR (x1,x2) -> + fID_OPT x1; + fFORMULA x2; + fNODE "CONSTR_to_RECCONSTR" 2 | CT_constr_coercion(x1, x2) -> - fID x1; + fID_OPT x1; fFORMULA x2; fNODE "constr_coercion" 2 and fRECCONSTR_LIST = function @@ -1244,7 +1247,7 @@ and fTACTIC_COM = function fLET_VALUE x2; fNODE "let_ltac" 2 | CT_lettac(x1, x2, x3) -> - fID x1; + fID_OPT x1; fFORMULA x2; fCLAUSE x3; fNODE "lettac" 3 |