fix sigma pruning when calling ltac, reachability is not correct

Author: gares

coq-builtin-synterp.elpi

@@ -306,10 +306,12 @@ external pred coq.env.current-section-path o:list string.
 kind clause type.
 type clause id -> grafting -> prop -> clause.
 
-% Specify if the clause has to be grafted before or after a named clause
+% Specify if the clause has to be grafted before, grafted after or replace
+% a named clause
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
 kind scope type.

coq-builtin.elpi

@@ -1711,10 +1711,12 @@ external pred coq.extra-dep i:id, o:option id.
 kind clause type.
 type clause id -> grafting -> prop -> clause.
 
-% Specify if the clause has to be grafted before or after a named clause
+% Specify if the clause has to be grafted before, grafted after or replace
+% a named clause
 kind grafting type.
 type before id -> grafting.
 type after id -> grafting.
+type replace id -> grafting.
 
 % Specify to which module the clause should be attached to
 kind scope type.

src/coq_elpi_HOAS.ml

@@ -2434,10 +2434,10 @@ let solution2evd sigma0 { API.Data.constraints; assignments; state; pp_ctx } roo
     get_declared_goals (Evar.Set.diff all_goals solved_goals) constraints state assignments pp_ctx in
   debug Pp.(fun () -> str "Goals: " ++ prlist_with_sep spc Evar.print declared_goals);
   debug Pp.(fun () -> str "Shelved Goals: " ++ prlist_with_sep spc Evar.print shelved_goals);
-  Evd.fold_undefined (fun k _ sigma ->
+(* wrong:  Evd.fold_undefined (fun k _ sigma ->
     if Evar.Set.mem k all_goals || Evd.mem sigma0 k then sigma
     else Evd.remove sigma k
-    ) sigma sigma,
+    ) sigma*) sigma,
   declared_goals,
   shelved_goals