From 829b998d08ec1bfcd68e82b42c369e1e35eb5bed Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 12 Jan 2010 12:23:37 +0000 Subject: [PATCH] Fixed a bug in the discrimination principle: the refiner was not able to synthesize the return type of the inner match correctly. --- helm/software/components/ng_tactics/nDestructTac.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml index 4f87707eb..8b2065a43 100644 --- a/helm/software/components/ng_tactics/nDestructTac.ml +++ b/helm/software/components/ng_tactics/nDestructTac.ml @@ -206,7 +206,8 @@ let mk_discriminator it status = Some (CicNotationPt.Binder (`Lambda, (mk_id "y",None), CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq";CicNotationPt.Implicit - `JustOne;CicNotationPt.Implicit `JustOne;mk_id "y"])), + `JustOne;(*CicNotationPt.Implicit `JustOne*) + mk_appl (mk_id (kname it i)::ts);mk_id "y"])), CicNotationPt.Implicit `JustOne ))), List.map (fun j -> -- 2.39.2