diff options
| author | Matthieu Sozeau | 2014-10-15 10:43:03 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-15 11:49:00 +0200 |
| commit | 04ee4f9160dec2d854bd45fcff4dac08ada39b61 (patch) | |
| tree | 360bf2853a7ab56a386faa207bf88881a3345eb7 /pretyping/reductionops.ml | |
| parent | 6bcb0ebf3552e544db8b3ac8f7d00beaec81059d (diff) | |
Implement a different strategy to expand primitive projections only when
required, i.e. in first-order unification cases where the head of the
other side is a hole or the eta-expanded constant.
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f545d29518..3819a92233 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -861,7 +861,7 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = let npars = pb.Declarations.proj_npars and arg = pb.Declarations.proj_arg in if not tactic_mode then - let stack' = (c, Stack.Proj (npars, arg, p, cst_l) :: stack) in + let stack' = (c, Stack.Proj (npars, arg, p, Cst_stack.empty (*cst_l*)) :: stack) in whrec Cst_stack.empty stack' else match ReductionBehaviour.get (Globnames.ConstRef kn) with | None -> @@ -1497,7 +1497,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = |args, (Stack.Proj (n,m,p,_) :: stack'') -> let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false (Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in - if isConstruct t_o && Projection.unfolded p then + if isConstruct t_o then whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'') else s,csts' |_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts' |