From f66e604a9d714ee9dba09234d935ee208bc89d97 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Nov 2015 22:36:48 +0100
Subject: Experimenting documentation of the Vars.subst functions.

Related questions:
- What balance to find between precision and conciseness?
- What convention to follow for typesetting the different components
  of the documentation is unclear?

New tentative type substl to emphasize that substitutions (for substl)
are represented the other way round compared to instances for
application (applist), though there are represented the same way
(i.e. most recent/dependent component on top) as instances of evars
(mkEvar).

Also removing unused subst*_named_decl functions (at least
substnl_named_decl is somehow non-sense).
---
 kernel/vars.ml | 21 +++++++--------------
 1 file changed, 7 insertions(+), 14 deletions(-)

(limited to 'kernel/vars.ml')

diff --git a/kernel/vars.ml b/kernel/vars.ml
index a800e25315..f8c0a65e64 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -151,6 +151,11 @@ let make_subst = function
   done;
   subst
 
+(* The type of substitutions, with term substituting most recent
+    binder at the head *)
+
+type substl = Constr.t list
+
 let substnl laml n c = substn_many (make_subst laml) n c
 let substl laml c = substn_many (make_subst laml) 0 c
 let subst1 lam c = substn_many [|make_substituend lam|] 0 c
@@ -159,13 +164,6 @@ let substnl_decl laml k r = map_rel_declaration (fun c -> substnl laml k c) r
 let substl_decl laml r = map_rel_declaration (fun c -> substnl laml 0 c) r
 let subst1_decl lam r = map_rel_declaration (fun c -> subst1 lam c) r
 
-let substnl_named_decl laml k d =
-  map_named_declaration (fun c -> substnl laml k c) d
-let substl_named_decl laml d =
-  map_named_declaration (fun c -> substnl laml 0 c) d
-let subst1_named_decl lam d =
-  map_named_declaration (fun c -> subst1 lam c) d
-
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
 let rec thin_val = function
@@ -197,15 +195,10 @@ let replace_vars var_alist x =
     in
     substrec 0 x
 
-(*
-let repvarkey = Profile.declare_profile "replace_vars";;
-let replace_vars vl c = Profile.profile2 repvarkey replace_vars vl c ;;
-*)
-
-(* (subst_var str t) substitute (VAR str) by (Rel 1) in t *)
+(* (subst_var str t) substitute (Var str) by (Rel 1) in t *)
 let subst_var str t = replace_vars [(str, Constr.mkRel 1)] t
 
-(* (subst_vars [id1;...;idn] t) substitute (VAR idj) by (Rel j) in t *)
+(* (subst_vars [id1;...;idn] t) substitute (Var idj) by (Rel j) in t *)
 let substn_vars p vars c =
   let _,subst =
     List.fold_left (fun (n,l) var -> ((n+1),(var,Constr.mkRel n)::l)) (p,[]) vars
-- 
cgit v1.2.3