diff options
| author | Gaëtan Gilbert | 2021-03-22 12:58:01 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2021-03-22 12:58:23 +0100 |
| commit | e27d1ad7f347ed50603625db29c81b60315c250f (patch) | |
| tree | 3c4341432727c4432e7b20e5db4452645e40a8ad /tactics | |
| parent | b3347fd5c3164dbe649bd819cdc0ef34b021b47a (diff) | |
[cbn internal] env is a regular positional argument
This is more consistent with other code.
Diffstat (limited to 'tactics')
| -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 |