🐛 Fix non uniform parameter check in lp2inductive_entry

There was an unneeded lift in the function comparing the non uniform parameters with the first binders of the type of each constructor. When testing by printing the terms, it looks like they are identical without the lift. With the lift, the match takes the last branch and wrongly outputs an error.

Author: ecranceMERCE

src/coq_elpi_HOAS.ml

@@ -2687,7 +2687,7 @@ let lp2inductive_entry ~depth coq_ctx constraints state t =
         (Context.Rel.Declaration.get_name x)
         (Context.Rel.Declaration.get_name y) &&
       EConstr.eq_constr_nounivs sigma
-       (EConstr.Vars.lift 1 (Context.Rel.Declaration.get_type x))
+       (Context.Rel.Declaration.get_type x)
        (Context.Rel.Declaration.get_type y) in
     let rec aux n nuparams params =
       match nuparams, params with