From d72e5c154faeea1d55387bc8c039d97f63ebd1c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 3 Mar 2019 21:03:37 +0100
Subject: Change the representation of kernel case.

We store bound variable names instead of functions for both branches and
predicate, and we furthermore add the parameters in the node. Let bindings
are not taken into account and require an environment lookup for retrieval.
---
 interp/impargs.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'interp')

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
-- 
cgit v1.2.3