From 4e44bd8331bf4d15c2e8e817f551a62d62288bcf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 25 Feb 2018 06:24:29 +0100
Subject: Deprecate undocumented "intros until 0" in favor of "intros *".

- The case 0 makes the code of intros until (and in particular of
  Detyping.lookup_quantified_hypothesis_as_displayed more complicated).
- The introduction pattern "*" is compositional while "until 0" is not.
---
 plugins/micromega/Tauto.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index 31f55ae9c3..458844e1b9 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -211,7 +211,7 @@ Set Implicit Arguments.
       (* BC *)
       simpl.
       case_eq (deduce t t) ; auto.
-      intros until 0.
+      intros *.
       case_eq (unsat t0) ; auto.
       unfold eval_clause.
       rewrite make_conj_cons. 
@@ -263,7 +263,7 @@ Set Implicit Arguments.
   Proof.
     induction cl.
     simpl. tauto.
-    intros until 0.
+    intros *.
     simpl.
     assert (HH := add_term_correct env a cl').
     case_eq (add_term a cl').
-- 
cgit v1.2.3