From e27d1ad7f347ed50603625db29c81b60315c250f Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 22 Mar 2021 12:58:01 +0100
Subject: [cbn internal] env is a regular positional argument

This is more consistent with other code.
---
 tactics/cbn.ml | 8 ++++----
 1 file 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
-- 
cgit v1.2.3