Merge pull request #76 from ppedrot/clean-equality-generic-rewrite-api

Adapt w.r.t. coq/coq#14449.
coq-community · Jun 7, 2021 · 16d30ab · 16d30ab
2 parents e1fe634 + 6475509
commit 16d30ab
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/src/coq.ml b/src/coq.ml
@@ -533,13 +533,13 @@ let rewrite ?(abort=false) hypinfo subst =
   let rew = build hypinfo subst in
   let tac =
     if not abort then    
-	  Equality.general_rewrite_bindings
-	    hypinfo.l2r
+	  Equality.general_rewrite ~where:None
+	    ~l2r:hypinfo.l2r
 	    Locus.AllOccurrences
-	    true (* tell if existing evars must be frozen for instantiation *)
-	    false
+	    ~freeze:true (* tell if existing evars must be frozen for instantiation *)
+	    ~dep:false
+	    ~with_evars:true
 	    (rew,Tactypes.NoBindings)
-	    true
     else
       Tacticals.New.tclIDTAC
   in tac