Imported Upstream version 8.5~beta3+dfsg

1 files changed, 35 insertions, 32 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index e11458c0..f3a48634 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -141,6 +141,7 @@ let progress_evars t =
 
 
 let e_give_exact flags poly (c,clenv) gl =
+  let (c, _, _) = c in
   let c, gl =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -149,36 +150,35 @@ let e_give_exact flags poly (c,clenv) gl =
 	c, {gl with sigma = clenv'.evd}
     else c, gl
   in
-  let t1 = pf_type_of gl c in
+  let t1 = pf_unsafe_type_of gl c in
     tclTHEN (Proofview.V82.of_tactic (Clenvtac.unify ~flags t1)) (exact_no_check c) gl
 
 let unify_e_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic (Clenvtac.clenv_refine true ~with_classes:false clenv') gls
+  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine true ~with_classes:false clenv'
 
 let unify_resolve poly flags (c,clenv) gls =
-  let clenv' = if poly then fst (Clenv.refresh_undefined_univs clenv) else clenv in
-  let clenv' = connect_clenv gls clenv' in
-  let clenv' = clenv_unique_resolver ~flags clenv' gls in
-  Proofview.V82.of_tactic 
-    (Clenvtac.clenv_refine false ~with_classes:false clenv') gls
+  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags clenv') gls in
+    Clenvtac.clenv_refine false ~with_classes:false clenv'
 
-let clenv_of_prods poly nprods (c, clenv) gls =
+let clenv_of_prods poly nprods (c, clenv) gl =
+  let (c, _, _) = c in
   if poly || Int.equal nprods 0 then Some clenv
   else
-    let ty = pf_type_of gls c in
+    let ty = Tacmach.New.pf_unsafe_type_of gl c in
     let diff = nb_prod ty - nprods in
       if Pervasives.(>=) diff 0 then
         (* Was Some clenv... *)
-	Some (mk_clenv_from_n gls (Some diff) (c,ty))
+	Some (Tacmach.New.of_old (fun gls -> mk_clenv_from_n gls (Some diff) (c,ty)) gl)
       else None
 
-let with_prods nprods poly (c, clenv) f gls =
-  match clenv_of_prods poly nprods (c, clenv) gls with
-  | None -> tclFAIL 0 (str"Not enough premisses") gls
-  | Some clenv' -> f (c, clenv') gls
+let with_prods nprods poly (c, clenv) f =
+  Proofview.Goal.nf_enter (fun gl ->
+  match clenv_of_prods poly nprods (c, clenv) gl with
+  | None -> Tacticals.New.tclZEROMSG (str"Not enough premisses")
+  | Some clenv' -> f (c, clenv') gl)
 
 (** Hack to properly solve dependent evars that are typeclasses *)
 
@@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	      (Hint_db.add_list hintl local_db) g'))) ::
+	      (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) ::
     (List.map (fun (x,_,_,_,_) -> x) 
      (e_trivial_resolve db_list local_db (project goal) (pf_concl goal)))
   in
@@ -205,7 +205,7 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
 	if cl.cl_strict then
 	  Evd.evars_of_term concl
 	else Evar.Set.empty
-    with _ -> Evar.Set.empty
+    with e when Errors.noncritical e -> Evar.Set.empty
   in
   let hintl =
     List.map_append
@@ -222,22 +222,23 @@ and e_my_find_search db_list local_db hdc complete sigma concl =
   let tac_of_hint =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
       let tac = function
-      | Res_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_resolve poly flags))
-      | ERes_pf (term,cl) -> Proofview.V82.tactic (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
+      | Res_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_resolve poly flags)
+      | ERes_pf (term,cl) -> with_prods nprods poly (term,cl) (unify_e_resolve poly flags)
       | Give_exact c -> Proofview.V82.tactic (e_give_exact flags poly c)
       | Res_pf_THEN_trivial_fail (term,cl) ->
-          Proofview.V82.tactic (tclTHEN (with_prods nprods poly (term,cl) (unify_e_resolve poly flags))
-            (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
+         Proofview.V82.tactic (tclTHEN
+				 (Proofview.V82.of_tactic ((with_prods nprods poly (term,cl) (unify_e_resolve poly flags))))
+				 (if complete then tclIDTAC else e_trivial_fail_db db_list local_db))
       | Unfold_nth c -> Proofview.V82.tactic (tclWEAK_PROGRESS (unfold_in_concl [AllOccurrences,c]))
       | Extern tacast -> conclPattern concl p tacast
       in
-      let tac = Proofview.V82.of_tactic (run_auto_tactic t tac) in
+      let tac = Proofview.V82.of_tactic (run_hint t tac) in
       let tac = if complete then tclCOMPLETE tac else tac in
-	match repr_auto_tactic t with
-	| Extern _ -> (tac,b,true, name, lazy (pr_autotactic t))
+	match repr_hint t with
+	| Extern _ -> (tac,b,true, name, lazy (pr_hint t))
 	| _ ->
 (* 	  let tac gl = with_pattern (pf_env gl) (project gl) flags p concl tac gl in *)
-	    (tac,b,false, name, lazy (pr_autotactic t))
+	    (tac,b,false, name, lazy (pr_hint t))
   in List.map tac_of_hint hintl
 
 and e_trivial_resolve db_list local_db sigma concl =
@@ -339,7 +340,7 @@ let make_hints g st only_classes sign =
 	  (PathOr (paths, path), hint @ hints)
       else (paths, hints))
     (PathEmpty, []) sign
-  in Hint_db.add_list hintlist (Hint_db.empty st true)
+  in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true)
 
 let make_autogoal_hints =
   let cache = ref (true, Environ.empty_named_context_val, 
@@ -374,7 +375,7 @@ let intro_tac : atac =
 	  let context = Environ.named_context_of_val (Goal.V82.hyps s g') in
 	  let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints)
 	    (true,false,false) info.only_classes None (List.hd context) in
-	  let ldb = Hint_db.add_list hint info.hints in
+	  let ldb = Hint_db.add_list env s hint info.hints in
 	    (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
       in {it = gls'; sigma = s;})
 
@@ -397,7 +398,7 @@ let is_unique env concl =
   try 
     let (cl,u), args = dest_class_app env concl in
       cl.cl_unique
-  with _ -> false
+  with e when Errors.noncritical e -> false
 
 let needs_backtrack env evd oev concl =
   if Option.is_empty oev || is_Prop env evd concl then
@@ -490,6 +491,7 @@ let hints_tac hints =
 let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk =
   let rec aux s (acc : autogoal list list) fk = function
     | (gl,info) :: gls ->
+        Control.check_for_interrupt ();
 	(match info.is_evar with
 	 | Some ev when Evd.is_defined s ev -> aux s acc fk gls
 	 | _ ->
@@ -842,6 +844,7 @@ let is_ground c gl =
 let autoapply c i gl =
   let flags = auto_unif_flags Evar.Set.empty 
     (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
-  let cty = pf_type_of gl c in
+  let cty = pf_unsafe_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  unify_e_resolve false flags (c,ce) gl
+  let tac = unify_e_resolve false flags ((c,cty,Univ.ContextSet.empty),ce) in
+  Proofview.V82.of_tactic (Proofview.Goal.nf_enter tac) gl