From 36f16f9b183c7324d8c8ff4851c6481a48296304 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 26 Jul 2006 14:05:31 +0000 Subject: [PATCH] Elim now performs whd to find the inductive type. --- helm/software/components/tactics/primitiveTactics.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 7a732a572..63c51d9ef 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -472,6 +472,7 @@ let elim_tac ~term = let (curi,metasenv,proofbo,proofty) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = ProofEngineHelpers.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in -- 2.39.2