some work for auto

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 366a9fe16f61ce3666767bec64cc3985ee69e648..a9b95339f88b28b39ecac12bff592fea5a0643df 100644 (file)
--- 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) ]