...

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index b7d06031bd73bf78b338123fbe04f6f6dbc95953..dd09178c2d70cc27073d183ad73abcd516c0a812 100644 (file)
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -233,9 +233,10 @@ let distribute_tac tac status =
        { gstatus = stack; istatus = sn }
 ;;
 
-(* attempt....
+(*
+
 type cic_term = NCic.conjecture
-type ast_term = CicNotationPt.term
+type ast_term = string * int * CicNotationPt.term
 type position = Ctx of NCic.context | Term of cic_term
 
 let relocate (name,ctx,t as term) context =
@@ -258,9 +259,9 @@ let disambiguate (status : lowtac_status) (t : ast_term)
  { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
 ;;
 
-let get_goal (status : low_status) (g : int) =
+let get_goal (status : lowtac_status) (g : int) =
  let _,_,metasenv,_,_ = status.pstatus in
- List.assoc goal metasenv
+ List.assoc g metasenv
 ;;
 
 let return ~orig status = 
@@ -270,19 +271,24 @@ let return ~orig status =
  status, open_goals, closed_goals
 ;;
 
-let apply t (status as orig,goal) =
- let goal = get_goal status goal in
- let status, t = disambiguate status t goal (Term goal) in
- let subst, metasenv = 
-   (goal, (name, context, t, gty)):: subst,
-   List.filter(fun (x,_) -> x <> goal) metasenv
- in
- return ~orig status
+let instantiate status i t =
+ let name,height,metasenv,subst,obj = status.pstatus in
+ let _, context, ty = List.assoc i metasenv in
+ let _,_,t = relocate t context in
+ let m = NCic.Meta (i,(0,NCic.Irl (List.length context))) in
+ let db = NCicUnifHint.db () in (* XXX fixme *)
+ let metasenv, subst = NCicUnification.unify db metasenv subst context m t in
+ { status with pstatus = (name,height,metasenv,subst,obj) }
 ;;
 
+let apply t (status as orig, goal) =
+ let goalty = get_goal status goal in
+ let status, t = disambiguate status t (Some goalty) (Term goalty) in
+ let status = instantiate status goal t in
+ return ~orig status
+;;
 *)
 
-
 let apply t (status,goal) =
  let uri,height,(metasenv as old_metasenv), subst,obj = status.pstatus in
  let name,context,gty = List.assoc goal metasenv in