some reorganization and some corrections

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / csub0_defs.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
index 7aa8a2c9bbff429c9457ebbdd02bcd9b5162601a..e96bef4a70a81ecbc1876aab4444379464fbaa98 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
@@ -118,7 +118,7 @@ Require Export ty0_defs.
       Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
                           (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1 : pr2_free *)
       XAuto.
 (* case 2 : pr2_delta *)
       CSub0Drop; XEAuto.