From a122a2e7980db0caad0141764440a970682737c3 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Thu, 20 Jan 2011 13:41:41 +0000 Subject: [PATCH] Bug fix for generation of elimination principles. --- helm/software/components/ng_tactics/nCicElim.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 4d32c197d..359d93bbd 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -116,7 +116,7 @@ let mk_elim uri leftno it (outsort,suffix) pragma = ) cl in let branches, branch_args = List.split branches_with_args in - let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in + let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in let final_params = List.map (function name -> name, None) params @ [p_name,Some p_ty] @ -- 2.39.5