Merge branch 'coq8.12' into coq8.13

coq-tactician · Jan 14, 2022 · 11203c3 · 11203c3
2 parents 31efe07 + 50123a4
commit 11203c3
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/stdlib-inject.patch b/stdlib-inject.patch
@@ -18,7 +18,7 @@ index ac5a69a38a..df188a5af7 100644
 -Declare ML Module "ltac_plugin".
 -
 -Export Set Default Proof Mode "Classic".
-+From Tactician Require Import Ltac1.Record.
++From Tactician Require Export Ltac1.Record.
 +Export Set Default Proof Mode "Tactician Ltac1".
 -- 
 2.34.0