Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

1 files changed, 5 insertions, 5 deletions

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 7742f985de..1e85fadce5 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -209,16 +209,16 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
         acc.(i) <- update pos rig acc.(i)
     | App (f,_) when rig && is_flexible_reference env sigma bound depth f ->
         if strict then () else
-          iter_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders env sigma push_lift (frec false) ed c
     | Proj (p, _) when rig ->
       if strict then () else
-        iter_with_full_binders sigma push_lift (frec false) ed c
+        iter_with_full_binders env sigma push_lift (frec false) ed c
     | Case _ when rig ->
         if strict then () else
-          iter_with_full_binders sigma push_lift (frec false) ed c
+          iter_with_full_binders env sigma push_lift (frec false) ed c
     | Evar _ -> ()
     | _ ->
-        iter_with_full_binders sigma push_lift (frec rig) ed c
+        iter_with_full_binders env sigma push_lift (frec rig) ed c
   in
   let () = if not (Vars.noccur_between sigma 1 bound m) then frec true (env,1) m in
   acc
@@ -228,7 +228,7 @@ let add_free_rels_until strict strongly_strict revpat bound env sigma m pos acc
 let rec is_rigid_head sigma t = match kind sigma t with
   | Rel _ | Evar _ -> false
   | Ind _ | Const _ | Var _ | Sort _ -> true
-  | Case (_,_,_,f,_) -> is_rigid_head sigma f
+  | Case (_,_,_,_,_,f,_) -> is_rigid_head sigma f
   | Proj (p,c) -> true
   | App (f,args) ->
       (match kind sigma f with