diff options
| author | msozeau | 2011-03-11 17:44:52 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-11 17:44:52 +0000 |
| commit | c70460837f5158325626b9412d8fa0651340b50f (patch) | |
| tree | 623b886c5e05567de8400315a8f0fd35589f6e03 /tactics | |
| parent | 56f7b49e1f46e495a215d65b7d2acaa03fe3b9cf (diff) | |
Keep information on which fields are subclasses in class declarations,
in preparation for adding forward reasoning to typeclass resolution.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13907 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml4 | 16 |
1 files changed, 1 insertions, 15 deletions
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index e3435191bf..df79bf3eef 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -59,7 +59,7 @@ let proper_class = let proper_proxy_class = lazy (class_info (Nametab.global (Qualid (dummy_loc, qualid_of_string "Coq.Classes.Morphisms.ProperProxy")))) -let proper_proj = lazy (mkConst (Option.get (snd (List.hd (Lazy.force proper_class).cl_projs)))) +let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs)))) let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) @@ -1387,20 +1387,6 @@ TACTIC EXTEND setoid_rewrite [ cl_rewrite_clause c o (occurrences_of occ) (Some id)] END -(* let occurrences_of l = (true,[]) *) - -(* VERNAC COMMAND EXTEND GenRew *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ) ] -> *) -(* [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id) ] -> *) -(* [ cl_rewrite_clause_newtac' c o (occurrences_of occ) (Some (snd id)) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> *) -(* [ cl_rewrite_clause_newtac' c o all_occurrences (Some (snd id)) ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> *) -(* [ cl_rewrite_clause_newtac' c o (occurrences_of occ) None ] *) -(* | [ "rew" orient(o) glob_constr_with_bindings(c) ] -> [ cl_rewrite_clause_newtac' c o all_occurrences None ] *) -(* END *) - let cl_rewrite_clause_newtac_tac c o occ cl gl = cl_rewrite_clause_newtac' c o occ cl; tclIDTAC gl |