diff options
| author | Pierre-Marie Pédrot | 2021-03-23 11:26:12 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-23 11:26:12 +0100 |
| commit | d3f78cad1532f000106ed0c0b8be2ac384ce1d3a (patch) | |
| tree | 60066276ea26f5cd999f8dfc88e3d28b0225ebaf | |
| parent | 1f7875b9c457aad27cd5ee8bfe2dd12898926cb2 (diff) | |
| parent | e27d1ad7f347ed50603625db29c81b60315c250f (diff) | |
Merge PR #13974: [cbn internal] env is a regular positional argument
Reviewed-by: ppedrot
| -rw-r--r-- | tactics/cbn.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/cbn.ml b/tactics/cbn.ml index 99d579f5c6..c3c61f6e51 100644 --- a/tactics/cbn.ml +++ b/tactics/cbn.ml @@ -453,7 +453,7 @@ let magically_constant_of_fixbody env sigma reference bd = function | None -> bd end -let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = +let contract_cofix env sigma ?reference (bodynum,(names,types,bodies as typedbodies)) = let nbodies = Array.length bodies in let make_Fi j = let ind = nbodies-j-1 in @@ -469,7 +469,7 @@ let contract_cofix ~env sigma ?reference (bodynum,(names,types,bodies as typedbo (** Similar to the "fix" case below *) let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = let raw_answer = - contract_cofix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in + contract_cofix env sigma ?reference:(Cst_stack.reference sigma cst_l) cofix in apply_subst (fun sigma x (t,sk') -> let t' = Cst_stack.best_replace sigma (mkCoFix cofix) cst_l t in @@ -479,7 +479,7 @@ let reduce_and_refold_cofix recfun env sigma cst_l cofix sk = (* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *) -let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = +let contract_fix env sigma ?reference ((recindices,bodynum),(names,types,bodies as typedbodies)) = let nbodies = Array.length recindices in let make_Fi j = let ind = nbodies-j-1 in @@ -498,7 +498,7 @@ let contract_fix ~env sigma ?reference ((recindices,bodynum),(names,types,bodies context" in contract_fix *) let reduce_and_refold_fix recfun env sigma cst_l fix sk = let raw_answer = - contract_fix ~env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in + contract_fix env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> let t' = Cst_stack.best_replace sigma (mkFix fix) cst_l t in |