diff options
| author | corbinea | 2004-06-29 15:55:40 +0000 |
|---|---|---|
| committer | corbinea | 2004-06-29 15:55:40 +0000 |
| commit | f68638477459eef68fb69adee244f58894e1f0a4 (patch) | |
| tree | 5555b399af00f9cdb5e91ccb291269af8c5afc19 /contrib/interface | |
| parent | 5a9ee53ca774a8878fd37812c114d82779657b16 (diff) | |
moved instantiate binding to extratactics
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5852 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index c772382e9f..ce44196d86 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1150,9 +1150,9 @@ and xlate_tac = CT_new_induction (xlate_int_or_constr a, xlate_using b, xlate_intro_patt_opt c) - | TacInstantiate (a, b, cl) -> + (*| TacInstantiate (a, b, cl) -> CT_instantiate(CT_int a, xlate_formula b, - assert false) + assert false) *) | TacLetTac (na, c, cl) -> CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, (* TODO LATER: This should be shared with Unfold, |