When rewriting in the local env, do not fail on identity rewriting

fix #463
EasyCrypt · Nov 8, 2023 · 9fd429a · 9fd429a
1 parent ff7b698
commit 9fd429a
Showing 1 changed file with 9 additions and 6 deletions.
diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml
@@ -1606,13 +1606,16 @@ let t_rewrite
       RApi.close tc (VRewrite (hd, rwpt));
       RApi.tcenv_of_rtcenv tc
 
-  | Some (h : ident) ->
-      let hyps = oget (LDecl.hyp_convert h (fun _ _ -> tgfp) (RApi.tc_hyps tc)) in
-      let hd   = RApi.newgoal tc ~hyps (RApi.tc_goal tc) in
-      let rwpt = { rpt_proof = pt; rpt_occrs = pos; rpt_lc = Some h; } in
+  | Some (h : ident) -> begin
+      match LDecl.hyp_convert h (fun _ _ -> tgfp) (RApi.tc_hyps tc) with
+      | Some hyps ->
+         let hd   = RApi.newgoal tc ~hyps (RApi.tc_goal tc) in
+         let rwpt = { rpt_proof = pt; rpt_occrs = pos; rpt_lc = Some h; } in
+         RApi.close tc (VRewrite (hd, rwpt))
 
-      RApi.close tc (VRewrite (hd, rwpt));
-      RApi.tcenv_of_rtcenv tc
+      | None -> ()
+    end;
+    RApi.tcenv_of_rtcenv tc
 
 (* -------------------------------------------------------------------- *)
 let t_rewrite_hyp ?xconv ?mode ?donot (id : EcIdent.t) pos (tc : tcenv1) =