Merge branch 'Deducteam:master' into master

Alidra · Oct 15, 2024 · d27c7d7 · d27c7d7
2 parents a63f1d6 + 7f6e007
commit d27c7d7
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 3 deletions.
diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml
@@ -145,6 +145,7 @@ let ind_data : popt -> Env.t -> term -> Sign.ind_data = fun pos env a ->
       begin
         try
           let ind = SymMap.find s !(sign.sign_ind) in
+          let _, ts = List.cut ts ind.ind_nb_params (*remove parameters*) in
           let ctxt = Env.to_ctxt env in
           if LibTerm.distinct_vars ctxt (Array.of_list ts) = None
           then fatal pos "%a is not applied to distinct variables." sym s

diff --git a/tests/OK/1141.lp b/tests/OK/1141.lp
@@ -0,0 +1,8 @@
+require open tests.OK.Set tests.OK.Prop tests.OK.Nat tests.OK.List;
+
+symbol sample_1 (list : 𝕃 nat) : π ⊤ ≔
+begin
+  induction
+    { apply ⊤ᵢ }
+    { assume x l ih; apply ih }
+end;
diff --git a/tests/OK/922.lp b/tests/OK/922.lp
@@ -20,5 +20,5 @@ with is0 (_ +1) ↪ false;
 
 opaque symbol s≠0 [n] : π (n +1 ≠ 0) ≔
 begin
-  assume n h; refine ind_eq h (λ n, istrue(is0 n)) top
+  assume n h; refine ind_eq h (λ n, istrue(is0 n)) ⊤ᵢ
 end;
diff --git a/tests/OK/Prop.lp b/tests/OK/Prop.lp
@@ -14,7 +14,7 @@ builtin "P" ≔ π;
 
 constant symbol ⊤ : Prop; // \top
 
-constant symbol top : π ⊤;
+constant symbol ⊤ᵢ : π ⊤;
 
 // false
 

diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh
@@ -60,7 +60,7 @@ do
         # proofs
         why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);;
         # "open"
-        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215);;
+        triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141);;
         # "inductive"
         strictly_positive_*|inductive|989|904|830|341);;
         # underscore in query