diff options
Diffstat (limited to 'tactics/g_rewrite.ml4')
| -rw-r--r-- | tactics/g_rewrite.ml4 | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 57dba7d61d..5e52debfcb 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -148,22 +148,6 @@ TACTIC EXTEND setoid_rewrite [ Proofview.V82.tactic (cl_rewrite_clause c o (occurrences_of occ) (Some id))] END -(* let cl_rewrite_clause_newtac_tac c o occ cl = *) -(* cl_rewrite_clause_newtac' c o occ cl *) - -(* TACTIC EXTEND GenRew *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> *) -(* [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> *) -(* [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) (Some id) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> *) -(* [ cl_rewrite_clause_newtac_tac c o AllOccurrences (Some id) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> *) -(* [ cl_rewrite_clause_newtac_tac c o (occurrences_of occ) None ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) ] -> *) -(* [ cl_rewrite_clause_newtac_tac c o AllOccurrences None ] *) -(* END *) - VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> |