oblivion ugraph everywhere outside the kernel

[helm.git] / helm / software / components / tactics / primitiveTactics.ml

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index e7632ebf4bf40c4bad2678b5ea23916b9e899796..53bfc39a9cf0e236a0a1bc1d5159ea0fb105571e 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -136,7 +136,7 @@ let eta_expand metasenv context t arg =
    List.map (function uri,t -> uri,aux n t)
   in
    let argty,_ = 
-    T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *)
+    T.type_of_aux' metasenv context arg CicUniv.oblivion_ugraph (* TASSI: FIXME *)
    in
     let fresh_name =
      FreshNamesGenerator.mk_fresh_name ~subst:[]
@@ -182,7 +182,7 @@ let
 =
  let module C = Cic in
   let params =
-    let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+    let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
     CicUtil.params_of_obj o
   in
    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
@@ -194,7 +194,7 @@ let
          [],[] -> []
        | uri::tl,[] ->
           let ty =
-            let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+            let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
               match o with
                   C.Variable (_,_,ty,_,_) ->
                     CicSubstitution.subst_vars !exp_named_subst_diff ty
@@ -242,7 +242,7 @@ let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termt
     goal_arity in
   let subst,newmetasenv',_ = 
    CicUnification.fo_unif_subst 
-     subst context newmetasenv consthead ty CicUniv.empty_ugraph
+     subst context newmetasenv consthead ty CicUniv.oblivion_ugraph
   in
   let t = 
     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
@@ -296,7 +296,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    in
    let metasenv' = metasenv@newmetasenvfragment in
    let termty,_ = 
-     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+     CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.oblivion_ugraph
    in
    let termty =
      CicSubstitution.subst_vars exp_named_subst_diff termty in
@@ -436,7 +436,7 @@ let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:
        (ProofEngineTypes.Fail (lazy
          "You can't letin a term containing the current goal"));
     let tty,_ =
-      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+      CicTypeChecker.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
      let fresh_name =
       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
@@ -464,7 +464,7 @@ let exact_tac ~term =
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
   let module T = CicTypeChecker in
   let module R = CicReduction in
-  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let ty_term,u = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
   if b then
    begin
@@ -614,7 +614,7 @@ let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
       | None, [], Some cpattern -> cpattern
       | _                       -> raise (PET.Fail (lazy "not implemented"))
    in    
-   let ugraph = CicUniv.empty_ugraph in
+   let ugraph = CicUniv.oblivion_ugraph in
    let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
    let conjecture = CicUtil.lookup_meta goal metasenv in
    let metano, context, ty = conjecture in 
@@ -721,7 +721,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let module C = Cic in
   let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+  let termty,_ = TC.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
   let termty = CicReduction.whd context termty in
   let (termty,metasenv',arguments,fresh_meta) =
    TermUtil.saturate_term
@@ -735,7 +735,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
     | _ -> raise NotAnInductiveTypeToEliminate
   in
   let paramsno,itty,patterns,right_args =
-    match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+    match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
     | C.InductiveDefinition (tys,_,paramsno,_),_ ->
        let _,left_parameters,right_args = 
          List.fold_right 
@@ -824,7 +824,7 @@ let cases_intros_tac ?(howmany=(-1)) ?(mk_fresh_name_callback = FreshNamesGenera
   let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
   let refined_term,_,metasenv'',_ = 
     CicRefine.type_of_aux' metasenv' context term_to_refine
-      CicUniv.empty_ugraph
+      CicUniv.oblivion_ugraph
   in
   let new_goals =
     ProofEngineHelpers.compare_metasenvs