diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-23 20:29:57 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-23 20:29:57 +0000 |
| commit | 22b169aae0a2731e04dfa296d86bb8bbcbe12c9f (patch) | |
| tree | fca90db9fb69b11b1a4eb1d9e6d958c73ba80536 /contrib/interface/centaur.ml4 | |
| parent | fe0bf68ccfe9ab635012b8e396011d20e8c25612 (diff) | |
Make sure proof by pointing works.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3605 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/centaur.ml4')
| -rw-r--r-- | contrib/interface/centaur.ml4 | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4 index fe25cb07d..f51570394 100644 --- a/contrib/interface/centaur.ml4 +++ b/contrib/interface/centaur.ml4 @@ -330,13 +330,11 @@ let globcv x = (ConstructRef ((sp, tyi), i))) | _ -> failwith "globcv : unexpected value";; -(* <\cpa> let pbp_tac_pcoq = pbp_tac (function (x:raw_tactic_expr) -> output_results (ctf_header "pbp_results" !global_request_id) (Some (P_t(xlate_tactic x))));; -</cpa> *) let blast_tac_pcoq = blast_tac (function (x:raw_tactic_expr) -> @@ -885,11 +883,12 @@ let command_creations = [ ];; *) -(* <\cpa> TACTIC EXTEND Pbp | [ "Pbp" ident_opt(idopt) natural_list(nl) ] -> [ if_pcoq pbp_tac_pcoq idopt nl ] END + +(* <\cpa> TACTIC EXTEND Blast | [ "Blast" ne_natural_list(nl) ] -> [ if_pcoq blast_tac_pcoq nl ] |