X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2FnCicSubstitution.ml;h=1e3856fff80447c48e20015518e013f153f422d1;hb=2a2ecad1d946365ccdf182d00480605b3497e7f5;hp=6c5bb4a9a5b07f9eb815bcf7e3d391fb44bd2935;hpb=f5ee9e3667439a473bac6b80f4b5865ee1c6b14a;p=helm.git

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