diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-12 17:46:18 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-24 17:35:20 +0200 |
| commit | d5d80dfc0f773fd6381ee4efefc74804d103fe4e (patch) | |
| tree | 73be62f93b8716b5b69fadf705a91e106dadec17 /plugins/cc | |
| parent | f5f4bb97634f4fac3dec766db27af994e745d749 (diff) | |
CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" function
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index fd46d8069..930ab333a 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -23,7 +23,9 @@ open Pp open CErrors open Util open Proofview.Notations -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let reference dir s = lazy (Coqlib.gen_reference "CC" dir s) @@ -155,7 +157,7 @@ let rec quantified_atom_of_constr env sigma nrels term = let patts=patterns_of_constr env sigma nrels atom in `Nrule patts else - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma (succ nrels) ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma (succ nrels) ff | _ -> let patts=patterns_of_constr env sigma nrels term in `Rule patts @@ -170,7 +172,7 @@ let litteral_of_constr env sigma term= else begin try - quantified_atom_of_constr (Environ.push_rel (LocalAssum (id,atom)) env) sigma 1 ff + quantified_atom_of_constr (Environ.push_rel (RelDecl.LocalAssum (id,atom)) env) sigma 1 ff with Not_found -> `Other (decompose_term env sigma term) end @@ -192,10 +194,10 @@ let make_prb gls depth additionnal_terms = ignore (add_term state t)) additionnal_terms; List.iter (fun decl -> - let (id,_,e) = Context.Named.Declaration.to_tuple decl in + let id = NamedDecl.get_id decl in begin let cid=mkVar id in - match litteral_of_constr env sigma e with + match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b | `Other ph -> |