From 659b5bdc713138a277c3b2adb71526536e1382e5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 16 Oct 2009 12:40:05 +0000 Subject: [PATCH] some work for auto --- helm/software/components/ng_tactics/nTactics.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 366a9fe16..a9b95339f 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -416,6 +416,7 @@ let generalize_tac ~where = List.fold_left (fun s t -> unify s (ctx_of goalty) canon t) status rest in let status, canon = term_of_cic_term status canon (ctx_of goalty) in + (* XXX embedding AST *) instantiate status goal (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; canon ])) ) s) ] -- 2.39.2