From bf7d2a3ad2535e7d57db79c17c81aaf67d956965 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 1 Jun 2014 10:26:41 +0200
Subject: Use of "H"-based names for propositional hypotheses obtained by
 destruction of schemes in Type such as sumbool.

Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).

This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.

Examples:

*** Non dependent case ***

Goal {True}+{False}-> True.
intros [|].

Before:

  t : True
  ============================
   True

and

  f : False
  ============================
   True

After:

  H : True
  ============================
   True

  H : False
  ============================
   True

*** Dependent case ***

Goal forall x:{True}+{False}, x=x.
intros [|].

Before:

  t : True
  ============================
   left t = left t

  f : False
  ============================
   right f = right f

After:

  HTrue : True
  ============================
   left HTrue = left HTrue

  HFalse : False
  ============================
   right HFalse = right HFalse
---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a3c8bf6f05..1847df58e6 100644
--- a/CHANGES
+++ b/CHANGES
@@ -590,6 +590,9 @@ Other tactics
   clears (resp. reverts) H and all the hypotheses that depend on H.
 - Ltac's pattern-matching now supports matching metavariables that
   depend on variables bound upwards in the pattern.
+- Case analysis on schemes in Type containing Proposition now produces
+  "H"-based names (important source of incompatibility that can be
+  repaired by using option "Unset Standard Proposition Elimination Names").
 
 Tactic definitions
 
-- 
cgit v1.2.3