Merge pull request #590 from FStarLang/gebner_amb_intro

gebner · web-flow · commit bb458522fe3f · 2026-03-11T14:35:25.000-07:00
Allow ambiguous unification in intro lemmas.
diff --git a/src/checker/Pulse.Checker.Prover.fst b/src/checker/Pulse.Checker.Prover.fst
@@ -1271,7 +1271,7 @@ let prove_step (pg: penv) (ctxt goals: list slprop_view)
     (fun _ -> prove_first g ctxt goals (prove_pure g ctxt false));
     (fun _ -> prove_first g ctxt goals (prove_with_pure g ctxt false));
     (fun _ -> prove_first g ctxt goals (eager_intro_lemma_step pg ctxt));
-    (fun _ -> prove_first g ctxt goals (intro_lemma_step try_prove_core { pg with penv_allow_amb = false } ctxt));
+    (fun _ -> prove_first g ctxt goals (intro_lemma_step try_prove_core pg ctxt));
   ]
 
 let rec try_prove_core (pg: penv) (ctxt goals: list slprop_view) : T.Tac (prover_result pg.penv_env ctxt goals) =

Original file line number	Diff line number	Diff line change
`@@ -1271,7 +1271,7 @@ let prove_step (pg: penv) (ctxt goals: list slprop_view)`
`1271`	`1271`	`(fun _ -> prove_first g ctxt goals (prove_pure g ctxt false));`
`1272`	`1272`	`(fun _ -> prove_first g ctxt goals (prove_with_pure g ctxt false));`
`1273`	`1273`	`(fun _ -> prove_first g ctxt goals (eager_intro_lemma_step pg ctxt));`
`1274`		`- (fun _ -> prove_first g ctxt goals (intro_lemma_step try_prove_core { pg with penv_allow_amb = false } ctxt));`
	`1274`	`+ (fun _ -> prove_first g ctxt goals (intro_lemma_step try_prove_core pg ctxt));`
`1275`	`1275`	`]`
`1276`	`1276`
`1277`	`1277`	`let rec try_prove_core (pg: penv) (ctxt goals: list slprop_view) : T.Tac (prover_result pg.penv_env ctxt goals) =`