From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 16 Oct 2009 12:40:05 +0000 (+0000)
Subject: some work for auto
X-Git-Tag: make_still_working~3289
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=659b5bdc713138a277c3b2adb71526536e1382e5;p=helm.git

some work for auto
---

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) ]