diff options
| author | herbelin | 2005-03-07 21:39:55 +0000 |
|---|---|---|
| committer | herbelin | 2005-03-07 21:39:55 +0000 |
| commit | d2562604fcea7ef0b0c5658af8fe21003ef3953e (patch) | |
| tree | 7fde3fe8bac6e069de13a153fda8844bd98a3a04 /contrib/interface | |
| parent | 3af4fe78c8e5ed1c4148e8feeffeb6c66eaa6b09 (diff) | |
Added 'clear - id' to clear all hypotheses except the ones dependent in the statement of id
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/pbp.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml index ef9f1280bc..5329556619 100644 --- a/contrib/interface/pbp.ml +++ b/contrib/interface/pbp.ml @@ -177,7 +177,7 @@ let make_pbp_atomic_tactic = function TacAtom (zz, TacElim ((make_var hyp_name,ExplicitBindings bind),None)) | PbpTryClear l -> - TacTry (TacAtom (zz, TacClear (List.map (fun s -> AI (zz,s)) l))) + TacTry (TacAtom (zz, TacClear (false,List.map (fun s -> AI (zz,s)) l))) | PbpSplit -> TacAtom (zz, TacSplit (false,NoBindings));; let rec make_pbp_tactic = function diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 60688b625f..1bf8e85fd5 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1125,11 +1125,12 @@ and xlate_tac = CT_decompose_list(CT_id_ne_list(id',l'),xlate_formula c) | TacDecomposeAnd c -> CT_decompose_record (xlate_formula c) | TacDecomposeOr c -> CT_decompose_sum(xlate_formula c) - | TacClear [] -> + | TacClear (false,[]) -> xlate_error "Clear expects a non empty list of identifiers" - | TacClear (id::idl) -> + | TacClear (false,id::idl) -> let idl' = List.map xlate_hyp idl in CT_clear (CT_id_ne_list (xlate_hyp id, idl')) + | TacClear (true,_) -> xlate_error "TODO: 'clear - idl' and 'clear'" | (*For translating tactics/Inv.v *) TacInversion (NonDepInversion (k,idl,l),quant_hyp) -> CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp, |