From 2a2ecad1d946365ccdf182d00480605b3497e7f5 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 12 Aug 2008 21:11:17 +0000 Subject: [PATCH] Fixed two legacy comments --- helm/software/components/ng_kernel/nCic.ml | 3 ++- helm/software/components/ng_kernel/nCicSubstitution.ml | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml index d3bc8d793..a9cc9a671 100644 --- a/helm/software/components/ng_kernel/nCic.ml +++ b/helm/software/components/ng_kernel/nCic.ml @@ -23,7 +23,8 @@ type implicit_annotation = [ `Closed | `Type | `Hole | `Term ] type lc_kind = Irl of int | Ctx of term list and local_context = int * lc_kind (* shift (0 -> no shift), - subst (None means id) *) + subst (Irl n means id of + length n) *) and term = | Rel of int (* DeBruijn index, 1 based *) | Meta of int * local_context diff --git a/helm/software/components/ng_kernel/nCicSubstitution.ml b/helm/software/components/ng_kernel/nCicSubstitution.ml index 6c5bb4a9a..1e3856fff 100644 --- a/helm/software/components/ng_kernel/nCicSubstitution.ml +++ b/helm/software/components/ng_kernel/nCicSubstitution.ml @@ -88,10 +88,10 @@ let rec psubst ?(avoid_beta_redexes=false) map_arg args = let subst ?avoid_beta_redexes arg = psubst ?avoid_beta_redexes (fun x -> x)[arg];; -(* subst_meta (n, Some [t_1 ; ... ; t_n]) t *) +(* subst_meta (n, C.Ctx [t_1 ; ... ; t_n]) t *) (* returns the term [t] where [Rel i] is substituted with [t_i] lifted by n *) (* [t_i] is lifted as usual when it crosses an abstraction *) -(* subst_meta (n, Non) t -> lift n t *) +(* subst_meta (n, (C.Irl _ | C.Ctx [])) t | -> lift n t *) let subst_meta = function | m, C.Irl _ | m, C.Ctx [] -> lift m -- 2.39.2