Fixed two legacy comments

[helm.git] / helm / software / components / ng_kernel / nCicSubstitution.ml

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