add clear * to clear all unused items in the context recursively

src/ecHiGoal.ml

@@ -163,17 +163,22 @@ let process_coq ~loc ~name (ttenv : ttenv) coqmode  pi (tc : tcenv1) =
     t_seq (t_simplify ~delta:`No) (t_coq ~loc ~name ~mode:(`Report (Some loc)) coqmode pi) tc
 
 (* -------------------------------------------------------------------- *)
-let process_clear symbols tc =
+let process_clear (info : clear_info) tc =
   let hyps = FApi.tc1_hyps tc in
-
   let toid s =
     if not (LDecl.has_name (unloc s) hyps) then
       tc_lookup_error !!tc ~loc:s.pl_loc `Local ([], unloc s);
     fst (LDecl.by_name (unloc s) hyps)
   in
-
-  try  t_clears (List.map toid symbols) tc
-  with (ClearError _) as err -> tc_error_exn !!tc err
+  match info with
+  | `Some symbols -> (
+    try  t_clears (List.map toid symbols) tc
+    with (ClearError _) as err -> tc_error_exn !!tc err)
+  | `All -> let try_clear tc id = 
+    (try t_clear1 id tc
+    with (ClearError _) -> tc) in
+    let hyp_ids = (List.map fst (LDecl.tohyps hyps).h_local) in
+    FApi.tcenv_of_tcenv1 (List.fold_left try_clear tc hyp_ids)
 
 (* -------------------------------------------------------------------- *)
 let process_algebra mode kind eqs (tc : tcenv1) =
@@ -1413,7 +1418,7 @@ let rec process_mintros_1 ?(cf = true) ttenv pis gs =
     t_simplify_lg ~delta:`IfApplied (ttenv, logic) tc
 
   and intro1_clear (_ : ST.state) xs tc =
-    process_clear xs tc
+    process_clear (`Some xs) tc
 
   and intro1_case (st : ST.state) nointro pis gs =
     let onsub gs =
@@ -1826,7 +1831,7 @@ let rec process_mgenintros ?cf ttenv pis tc =
       | `Gen gn ->
          t_onall (
            t_seqs [
-               process_clear gn.pr_clear;
+               process_clear (`Some gn.pr_clear);
                process_generalize gn.pr_genp
            ]) tc
     in process_mgenintros ~cf:false ttenv pis tc
@@ -1838,7 +1843,7 @@ let process_genintros ?cf ttenv pis tc =
 (* -------------------------------------------------------------------- *)
 let process_move ?doeq views pr (tc : tcenv1) =
   t_seqs
-    [process_clear pr.pr_clear;
+    [process_clear (`Some pr.pr_clear);
      process_generalize ?doeq pr.pr_genp;
      process_view views]
     tc
@@ -2078,7 +2083,7 @@ let process_case ?(doeq = false) gp tc =
             | _ -> ()
           end;
           t_seqs
-            [process_clear gp.pr_rev.pr_clear; t_case f;
+            [process_clear (`Some gp.pr_rev.pr_clear); t_case f;
              t_simplify_with_info EcReduction.betaiota_red]
             tc
 

src/ecHiGoal.mli

@@ -71,7 +71,7 @@ val process_mgenintros  : ?cf:bool -> ttenv -> introgenpattern list -> tactical
 val process_genintros   : ?cf:bool -> ttenv -> introgenpattern list -> backward
 val process_generalize  : ?doeq:bool -> genpattern list -> backward
 val process_move        : ?doeq:bool -> ppterm list -> prevert -> backward
-val process_clear       : psymbol list -> backward
+val process_clear       : clear_info -> backward
 val process_smt         : ?loc:EcLocation.t -> ttenv -> pprover_infos option -> backward
 val process_coq         : loc:EcLocation.t -> name:string -> ttenv -> EcProvers.coq_mode option -> pprover_infos -> backward
 val process_apply       : implicits:bool -> apply_t * prevert option -> backward

src/ecParser.mly

@@ -2682,8 +2682,11 @@ logtactic:
 | MOVE vw=prefix(SLASH, pterm)* gp=prefix(COLON, revert)?
    { Pmove { pr_rev = odfl prevert0 gp; pr_view = vw; } }
 
+| CLEAR STAR
+   { Pclear `All }
+
 | CLEAR l=loc(ipcore_name)+
-   { Pclear l }
+   { Pclear (`Some l) }
 
 | CONGR
    { Pcongr }

src/ecParsetree.ml

@@ -957,6 +957,12 @@ type apply_info = [
   | `ExactType of pqsymbol
 ]
 
+(* -------------------------------------------------------------------- *)
+type clear_info = [
+  | `All
+  | `Some of psymbol list
+]
+
 (* -------------------------------------------------------------------- *)
 type pgenhave = psymbol * intropattern option * psymbol list * pformula
 
@@ -979,7 +985,7 @@ type logtactic =
   | Pcut        of pcut
   | Pcutdef     of (intropattern * pcutdef)
   | Pmove       of prevertv
-  | Pclear      of psymbol list
+  | Pclear      of clear_info
   | Prewrite    of (rwarg list * osymbol_r)
   | Prwnormal   of pformula * pqsymbol list
   | Psubst      of pformula list