From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Sat, 13 Aug 2016 18:11:22 +0200
Subject: CLEANUP: minor readability improvements

mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.

If multiple modules define a function with a same name, e.g.:

	Context.{Rel,Named}.get_type

those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.
---
 plugins/decl_mode/decl_proof_instr.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6a28723b89..8e6c7a70d9 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -32,6 +32,9 @@ open Misctypes
 open Sigma.Notations
 open Context.Named.Declaration
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Strictness option *)
 
 let clear ids { it = goal; sigma } =
@@ -247,7 +250,7 @@ let close_previous_case pts =
 
 let filter_hyps f gls =
   let filter_aux id =
-    let id = get_id id in
+    let id = NamedDecl.get_id id in
     if f id then
       tclIDTAC
     else
@@ -357,8 +360,7 @@ let enstack_subsubgoals env se stack gls=
 		  let nlast=succ last in
 		  let (llast,holes,metas) =
 		    meta_aux nlast (mkMeta nlast :: lenv) q in
-                    let open Context.Rel.Declaration in
-		    (llast,holes,(nlast,special_nf gls (substl lenv (get_type decl)))::metas) in
+		    (llast,holes,(nlast,special_nf gls (substl lenv (RelDecl.get_type decl)))::metas) in
 	    let (nlast,holes,nmetas) =
 		meta_aux se.se_last_meta [] (List.rev rc) in
 	    let refiner = applist (appterm,List.rev holes) in
@@ -822,7 +824,7 @@ let define_tac id args body gls =
 let cast_tac id_or_thesis typ gls =
   match id_or_thesis with
     | This id ->
-        Proofview.V82.of_tactic  (pf_get_hyp gls id |> set_id id |> set_type typ |> convert_hyp) gls
+        Proofview.V82.of_tactic  (pf_get_hyp gls id |> NamedDecl.set_id id |> NamedDecl.set_type typ |> convert_hyp) gls
     | Thesis (For _ ) ->
 	error "\"thesis for ...\" is not applicable here."
     | Thesis Plain ->
-- 
cgit v1.2.3