Imported Upstream version 8.5~beta1+dfsg

1 files changed, 42 insertions, 39 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index b54e2323..18883df2 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -1,30 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Util
 open Names
-open Nameops
 open Term
 open Termops
-open Sign
-open Environ
 open Evd
-open Evarutil
-open Proof_type
 open Refiner
 open Logic
 open Reduction
-open Reductionops
 open Tacmach
-open Glob_term
-open Pattern
-open Tacexpr
 open Clenv
 
 
@@ -39,6 +29,7 @@ let clenv_cast_meta clenv =
     match kind_of_term u with
       | App _ | Case _ -> crec_hd u
       | Cast (c,_,_) when isMeta c -> u
+      | Proj (p, c) -> mkProj (p, crec_hd c)
       | _  -> map_constr crec u
 
   and crec_hd u =
@@ -53,6 +44,7 @@ let clenv_cast_meta clenv =
       | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
       | Case(ci,p,c,br) ->
 	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+      | Proj (p, c) -> mkProj (p, crec_hd c)
       | _ -> u
   in
   crec
@@ -62,67 +54,78 @@ let clenv_value_cast_meta clenv =
 
 let clenv_pose_dependent_evars with_evars clenv =
   let dep_mvs = clenv_dependent clenv in
-  if dep_mvs <> [] & not with_evars then
+  if not (List.is_empty dep_mvs) && not with_evars then
     raise
       (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-let clenv_refine with_evars ?(with_classes=true) clenv gls =
+let clenv_refine with_evars ?(with_classes=true) clenv =
+  (** ppedrot: a Goal.enter here breaks things, because the tactic below may
+      solve goals by side effects, while the compatibility layer keeps those
+      useless goals. That deserves a FIXME. *)
+  Proofview.V82.tactic begin fun gl ->
   let clenv = clenv_pose_dependent_evars with_evars clenv in
   let evd' =
     if with_classes then
-      Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
+      let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
         ~fail:(not with_evars) clenv.env clenv.evd
+      in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
   tclTHEN
-    (tclEVARS evd')
-    (refine (clenv_cast_meta clenv (clenv_value clenv)))
-    gls
+    (tclEVARS (Evd.clear_metas evd'))
+    (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
+  end
 
 open Unification
 
 let dft = default_unify_flags
 
-let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
-  clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
-
-let elim_res_pf_THEN_i clenv tac gls =
-  let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
-  tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
-
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
-
+let res_pf ?(with_evars=false) ?(with_classes=true) ?(flags=dft ()) clenv =
+  Proofview.Goal.enter begin fun gl ->
+    let clenv gl = clenv_unique_resolver ~flags clenv gl in
+    clenv_refine with_evars ~with_classes (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
+  end
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
    particulier ne semblent pas vérifier que des instances différentes
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
-let fail_quick_unif_flags = {
+let fail_quick_core_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly_in_conv_on_closed_terms = false;
+  use_evars_eagerly_in_conv_on_closed_terms = false;
   modulo_delta = empty_transparent_state;
   modulo_delta_types = full_transparent_state;
-  modulo_delta_in_merge = None;
   check_applied_meta_types = false;
-  resolve_evars = false;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = true; (* ? *)
-  frozen_evars = ExistentialSet.empty;
+  frozen_evars = Evar.Set.empty;
   restrict_conv_on_strict_subterms = false; (* ? *)
   modulo_betaiota = false;
   modulo_eta = true;
-  allow_K_in_toplevel_higher_order_unification = false
 }
 
-(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms ?(flags=fail_quick_unif_flags) m n gls =
-  let env = pf_env gls in
-  let evd = create_goal_evar_defs (project gls) in
-  let evd' = w_unify env evd CONV ~flags m n in
-  tclIDTAC {it = gls.it; sigma =  evd'}
+let fail_quick_unif_flags = {
+  core_unify_flags = fail_quick_core_unif_flags;
+  merge_unify_flags = fail_quick_core_unif_flags;
+  subterm_unify_flags = fail_quick_core_unif_flags;
+  allow_K_in_toplevel_higher_order_unification = false;
+  resolve_evars = false
+}
 
-let unify ?(flags=fail_quick_unif_flags) m gls =
-  let n = pf_concl gls in unifyTerms ~flags m n gls
+(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
+let unify ?(flags=fail_quick_unif_flags) m =
+  Proofview.Goal.enter begin fun gl ->
+    let env = Tacmach.New.pf_env gl in
+    let n = Tacmach.New.pf_nf_concl gl in
+    let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
+    try
+      let evd' = w_unify env evd CONV ~flags m n in
+	Proofview.Unsafe.tclEVARSADVANCE evd'
+    with e when Errors.noncritical e ->
+      (** This is Tacticals.tclFAIL *)
+      Proofview.tclZERO (FailError (0, lazy (Errors.print e)))
+  end