[ porting from CerCo's Matita ]

[helm.git] / matita / components / ng_tactics / nTacStatus.ml

diff --git a/matita/components/ng_tactics/nTacStatus.ml b/matita/components/ng_tactics/nTacStatus.ml
index fbcdccb31c3810604abb967e4492ca007514d345..dd763c3272fdc812623a62250a77b1394ca1ea65 100644 (file)
--- a/matita/components/ng_tactics/nTacStatus.ml
+++ b/matita/components/ng_tactics/nTacStatus.ml
@@ -66,7 +66,7 @@ class auto_status =
 
 class type g_pstatus =
  object
-  inherit LexiconTypes.g_status
+  inherit GrafiteDisambiguate.g_status
   inherit g_auto_status
   inherit g_eq_status
   method obj: NCic.obj
@@ -75,7 +75,7 @@ class type g_pstatus =
 class pstatus =
  fun (o: NCic.obj) ->
  object (self)
-   inherit LexiconTypes.status
+   inherit GrafiteDisambiguate.status
    inherit auto_status
    inherit eq_status
    val obj = o
@@ -83,7 +83,7 @@ class pstatus =
    method set_obj o = {< obj = o >}
    method set_pstatus : 'status. #g_pstatus as 'status -> 'self
    = fun o ->
-    (((self#set_lexicon_engine_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
+    (((self#set_disambiguate_status o)#set_obj o#obj)#set_auto_status o)#set_eq_status o
   end
 
 type tactic_term = NotationPt.term Disambiguate.disambiguator_input
@@ -195,7 +195,7 @@ let disambiguate status context t ty =
  in
  let uri,height,metasenv,subst,obj = status#obj in
  let metasenv, subst, status, t = 
-   GrafiteDisambiguate.disambiguate_nterm expty status context metasenv subst t 
+   GrafiteDisambiguate.disambiguate_nterm status expty context metasenv subst t 
  in
  let new_pstatus = uri,height,metasenv,subst,obj in
   status#set_obj new_pstatus, (context, t) 
@@ -287,11 +287,15 @@ let to_subst status i entry =
   status#set_obj (name,height,metasenv,subst,obj)
 ;;
 
-let instantiate status i t =
+let instantiate status ?refine:(dorefine=true) i t =
  let _,_,metasenv,_,_ = status#obj in
  let gname, context, gty = List.assoc i metasenv in
- let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
-  to_subst status i (gname,context,t,ty)
+  if dorefine then
+   let status, (_,t), (_,ty) = refine status context t (Some (context,gty)) in
+    to_subst status i (gname,context,t,ty)
+  else
+   let status,(_,ty) = typeof status context t in
+    to_subst status i (gname,context,snd t,ty)
 ;;
 
 let instantiate_with_ast status i t =