diff options
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 25091f783..f363deac6 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -92,7 +92,7 @@ let destruct_on_using c id = let destruct_on_as c l = destruct false None c (Some (dl,l)) None -(* reconstruct the inductive with the correct deBruijn indexes *) +(* reconstruct the inductive with the correct de Bruijn indexes *) let mkFullInd (ind,u) n = let mib = Global.lookup_mind (fst ind) in let nparams = mib.mind_nparams in @@ -171,7 +171,7 @@ let build_beq_scheme mode kn = (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) - eqA = the deBruijn index of the first eq param + eqA = the de Bruijn index of the first eq param ndx = how much to translate due to the 2nd Case *) let compute_A_equality rel_list nlist eqA ndx t = |