From 275449f6cc7da843aae2e0455edc38fda8571aec Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 6 Oct 2009 14:38:00 +0000 Subject: [PATCH] fixed constructor on non inductive type --- helm/software/components/ng_tactics/nTacStatus.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nTacStatus.ml b/helm/software/components/ng_tactics/nTacStatus.ml index 2b310ff38..41319b473 100644 --- a/helm/software/components/ng_tactics/nTacStatus.ml +++ b/helm/software/components/ng_tactics/nTacStatus.ml @@ -14,6 +14,8 @@ exception Error of string lazy_t * exn option let fail ?exn msg = raise (Error (msg,exn)) +module NRef = NReference + let wrap f x = try f x with @@ -334,7 +336,8 @@ let analyse_indty status ty = let ref, args = match reduct with | _,NCic.Const ref -> ref, [] - | _,NCic.Appl (NCic.Const ref :: args) -> ref, args + | _,NCic.Appl (NCic.Const (NRef.Ref (_,(NRef.Ind _)) as ref) :: args) -> + ref, args | _,_ -> fail (lazy ("not an inductive type")) in let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in let _,_,_,cl = List.nth tl i in -- 2.39.2