Fixed two legacy comments

diff --git a/helm/software/components/ng_kernel/nCic.ml b/helm/software/components/ng_kernel/nCic.ml
index d3bc8d793730e7cf8c6b1dc471b254beb98063f4..a9cc9a671f39161afc8500eec4f012d2769fc589 100644 (file)
--- 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 6c5bb4a9a5b07f9eb815bcf7e3d391fb44bd2935..1e3856fff80447c48e20015518e013f153f422d1 100644 (file)
--- 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