add exclude filters and test

src/ecHiGoal.ml

@@ -171,14 +171,16 @@ let process_clear (info : clear_info) tc =
     fst (LDecl.by_name (unloc s) hyps)
   in
   match info with
-  | `Some symbols -> (
+  | `Include symbols -> (
     try  t_clears (List.map toid symbols) tc
     with (ClearError _) as err -> tc_error_exn !!tc err)
-  | `All -> let try_clear tc id = 
+  | `Exclude symbols -> 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 excluded = List.map toid symbols in
+    let hyp_ids = List.map fst (LDecl.tohyps hyps).h_local in
+    let clear_list = List.filter (fun x -> not (List.mem x excluded)) hyp_ids in
+    FApi.tcenv_of_tcenv1 (List.fold_left try_clear tc clear_list)
 
 (* -------------------------------------------------------------------- *)
 let process_algebra mode kind eqs (tc : tcenv1) =
@@ -1418,7 +1420,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 (`Some xs) tc
+    process_clear (`Include xs) tc
 
   and intro1_case (st : ST.state) nointro pis gs =
     let onsub gs =
@@ -1831,7 +1833,7 @@ let rec process_mgenintros ?cf ttenv pis tc =
       | `Gen gn ->
          t_onall (
            t_seqs [
-               process_clear (`Some gn.pr_clear);
+               process_clear (`Include gn.pr_clear);
                process_generalize gn.pr_genp
            ]) tc
     in process_mgenintros ~cf:false ttenv pis tc
@@ -1843,7 +1845,7 @@ let process_genintros ?cf ttenv pis tc =
 (* -------------------------------------------------------------------- *)
 let process_move ?doeq views pr (tc : tcenv1) =
   t_seqs
-    [process_clear (`Some pr.pr_clear);
+    [process_clear (`Include pr.pr_clear);
      process_generalize ?doeq pr.pr_genp;
      process_view views]
     tc
@@ -2083,7 +2085,7 @@ let process_case ?(doeq = false) gp tc =
             | _ -> ()
           end;
           t_seqs
-            [process_clear (`Some gp.pr_rev.pr_clear); t_case f;
+            [process_clear (`Include gp.pr_rev.pr_clear); t_case f;
              t_simplify_with_info EcReduction.betaiota_red]
             tc
 

src/ecParser.mly

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

src/ecParsetree.ml

@@ -959,8 +959,8 @@ type apply_info = [
 
 (* -------------------------------------------------------------------- *)
 type clear_info = [
-  | `All
-  | `Some of psymbol list
+  | `Exclude of psymbol list
+  | `Include of psymbol list
 ]
 
 (* -------------------------------------------------------------------- *)

tests/clear.ec

@@ -0,0 +1,21 @@
+lemma L: true.
+pose x:=false.
+clear x.
+(* `x` is now unbound *)
+pose x:=false.
+pose y:=x.
+pose z:=y.
+clear -y. 
+(* `z` is unbound, but `x` is not, since `y` depends on it *)
+pose z:=x.
+clear y.
+pose y:=z.
+clear. 
+(* everything is unbound, since nothing is in the goal *)
+pose x:=true.
+pose y:=false.
+clear. 
+(* we cannot clear `x` since it is in the goal,
+   but `y` is not used so it becomes unbound *)
+pose y:= x.
+abort.