Merge branch 'v8.6'

4 files changed, 64 insertions, 65 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f9f8e8715..96767e7f6 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -45,7 +45,11 @@ let typeclasses_modulo_eta = ref false
 let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d
 let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta
 
-let typeclasses_limit_intros = ref false
+(** When this flag is enabled, the resolution of type classes tries to avoid
+    useless introductions. This is no longer useful since we have eta, but is
+    here for compatibility purposes. Another compatibility issues is that the
+    cost (in terms of search depth) can differ. *)
+let typeclasses_limit_intros = ref true
 let set_typeclasses_limit_intros d = (:=) typeclasses_limit_intros d
 let get_typeclasses_limit_intros () = !typeclasses_limit_intros
 
@@ -57,31 +61,22 @@ let typeclasses_iterative_deepening = ref false
 let set_typeclasses_iterative_deepening d = (:=) typeclasses_iterative_deepening d
 let get_typeclasses_iterative_deepening () = !typeclasses_iterative_deepening
 
-let get_compat_version d =
-  match d with
-  | "8.5" -> Flags.V8_5
-  | _ -> Flags.Current
-
-let typeclasses_unif_compat = ref Flags.V8_5
-let set_typeclasses_unif_compat d =
-  if d == Flags.Current then set_typeclasses_limit_intros false
-  else set_typeclasses_limit_intros true;
-  (:=) typeclasses_unif_compat d
-
-let get_typeclasses_unif_compat () = !typeclasses_unif_compat
-let set_typeclasses_unif_compat_string d =
-  set_typeclasses_unif_compat (get_compat_version d)
-let get_typeclasses_unif_compat_string () =
-  Flags.pr_version (get_typeclasses_unif_compat ())
-
-let typeclasses_compat = ref Flags.Current
-let set_typeclasses_compat d = (:=) typeclasses_compat d
-let get_typeclasses_compat () = !typeclasses_compat
-let set_typeclasses_compat_string d =
-  set_typeclasses_compat (get_compat_version d)
-
-let get_typeclasses_compat_string () =
-  Flags.pr_version (get_typeclasses_compat ())
+(** [typeclasses_filtered_unif] governs the unification algorithm used by type
+    classes. If enabled, a new algorithm based on pattern filtering and refine
+    will be used. When disabled, the previous algorithm based on apply will be
+    used. *)
+let typeclasses_filtered_unification = ref false
+let set_typeclasses_filtered_unification d =
+  (:=) typeclasses_filtered_unification d
+let get_typeclasses_filtered_unification () =
+  !typeclasses_filtered_unification
+
+(** [typeclasses_legacy_resolution] falls back to the 8.5 resolution algorithm,
+    instead of the 8.6 one which uses the native backtracking facilities of the
+    proof engine. *)
+let typeclasses_legacy_resolution = ref false
+let set_typeclasses_legacy_resolution d = (:=) typeclasses_legacy_resolution d
+let get_typeclasses_legacy_resolution () = !typeclasses_legacy_resolution
 
 let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0)
 let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false
@@ -135,22 +130,22 @@ let _ =
       optwrite = set_typeclasses_iterative_deepening; }
 
 let _ =
-  declare_string_option
+  declare_bool_option
     { optsync  = true;
       optdepr  = false;
       optname  = "compat";
-      optkey   = ["Typeclasses";"Compatibility"];
-      optread  = get_typeclasses_compat_string;
-      optwrite = set_typeclasses_compat_string; }
+      optkey   = ["Typeclasses";"Legacy";"Resolution"];
+      optread  = get_typeclasses_legacy_resolution;
+      optwrite = set_typeclasses_legacy_resolution; }
 
 let _ =
-  declare_string_option
+  declare_bool_option
     { optsync  = true;
       optdepr  = false;
       optname  = "compat";
-      optkey   = ["Typeclasses";"Unification";"Compatibility"];
-      optread  = get_typeclasses_unif_compat_string;
-      optwrite = set_typeclasses_unif_compat_string; }
+      optkey   = ["Typeclasses";"Filtered";"Unification"];
+      optread  = get_typeclasses_filtered_unification;
+      optwrite = set_typeclasses_filtered_unification; }
 
 let set_typeclasses_debug =
   declare_bool_option
@@ -402,7 +397,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
     fun (flags, {pri = b; pat = p; poly = poly; code = t; name = name}) ->
       let tac = function
         | Res_pf (term,cl) ->
-           if get_typeclasses_unif_compat () = Flags.Current then
+           if get_typeclasses_filtered_unification () then
              let tac =
                with_prods nprods poly (term,cl)
                           ({ enter = fun gl clenv ->
@@ -412,13 +407,13 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
            else
              let tac =
                with_prods nprods poly (term,cl) (unify_resolve poly flags) in
-             if get_typeclasses_compat () = Flags.V8_5 then
+             if get_typeclasses_legacy_resolution () then
                Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
              else
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
         | ERes_pf (term,cl) ->
-           if get_typeclasses_unif_compat () = Flags.Current then
+           if get_typeclasses_filtered_unification () then
              let tac = (with_prods nprods poly (term,cl)
                   ({ enter = fun gl clenv ->
                              (matches_pattern concl p) <*>
@@ -427,7 +422,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
            else
              let tac =
                with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
-             if get_typeclasses_compat () = Flags.V8_5 then
+             if get_typeclasses_legacy_resolution () then
                Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
              else
                Proofview.tclBIND (Proofview.with_shelf tac)
@@ -447,7 +442,7 @@ and e_my_find_search db_list local_db hdc complete only_classes sigma concl =
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
       let pp =
         match p with
-        | Some pat when get_typeclasses_unif_compat () = Flags.Current ->
+        | Some pat when get_typeclasses_filtered_unification () ->
            str " with pattern " ++ Printer.pr_constr_pattern pat
         | _ -> mt ()
       in
@@ -1293,7 +1288,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state)
   in
   let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in
   let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in
-  if get_typeclasses_compat () = Flags.V8_5 then
+  if get_typeclasses_legacy_resolution () then
     Proofview.V82.tactic
     (fun gl ->
       try V85.eauto85 depth ~only_classes ~st dbs gl
@@ -1419,10 +1414,10 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
         let evd' =
-          if get_typeclasses_compat () = Flags.Current then
-            Search.typeclasses_resolve debug depth unique p evd
-          else
+          if get_typeclasses_legacy_resolution () then
             V85.resolve_all_evars_once debug depth unique p evd
+          else
+            Search.typeclasses_resolve debug depth unique p evd
         in
          if has_undefined p oevd evd' then raise Unresolved;
          docomp evd' comps
@@ -1467,12 +1462,13 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   let st = Hint_db.transparent_state hints in
   let depth = get_typeclasses_depth () in
   let gls' =
-    if get_typeclasses_compat () = Flags.Current then
+    if get_typeclasses_legacy_resolution () then
+      V85.eauto85 depth ~st [hints] gls
+    else
       try
         Proofview.V82.of_tactic
         (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls
       with Refiner.FailError _ -> raise Not_found
-    else V85.eauto85 depth ~st [hints] gls
   in
   let evd = sig_sig gls' in
   let t' = let (ev, inst) = destEvar t in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 444fac170..7c819edad 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -702,16 +702,16 @@ let replace_in_clause_maybe_by c1 c2 cl tac_opt =
 exception DiscrFound of
   (constructor * int) list * constructor * constructor
 
-let injection_on_proofs = ref false
+let keep_proof_equalities_for_injection = ref false
 
 let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
       optname  = "injection on prop arguments";
-      optkey   = ["Injection";"On";"Proofs"];
-      optread  = (fun () -> !injection_on_proofs) ;
-      optwrite = (fun b -> injection_on_proofs := b) }
+      optkey   = ["Keep";"Proof";"Equalities"];
+      optread  = (fun () -> !keep_proof_equalities_for_injection) ;
+      optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
 
 let find_positions env sigma t1 t2 =
@@ -756,7 +756,7 @@ let find_positions env sigma t1 t2 =
 	    project env sorts posn t1_0 t2_0
   in
   try
-    let sorts = if !injection_on_proofs then [InSet;InType;InProp]
+    let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
 		else [InSet;InType]
     in
     Inr (findrec sorts [] t1 t2)
@@ -1390,7 +1390,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   | Inl _ ->
      tclZEROMSG (strbrk"This equality is discriminable. You should use the discriminate tactic to solve the goal.")
   | Inr [] ->
-     let suggestion = if !injection_on_proofs then "" else " You can try to use option Set Injection On Proofs." in
+     let suggestion =
+         if !keep_proof_equalities_for_injection then
+            "" else
+            " You can try to use option Set Keep Proof Equalities." in
      tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
   | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
      tclZEROMSG (str"Nothing to inject.")
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d80e86241..10fc5076c 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -204,11 +204,11 @@ let inversion_scheme env sigma t sort dep_option inv_op =
       tclTHEN intro (onLastHypId inv_op)) pf)
   in
   let pfterm = List.hd (Proof.partial_proof pf) in
-  let global_named_context = Global.named_context () in
+  let global_named_context = Global.named_context_val () in
   let ownSign = ref begin
     fold_named_context
       (fun env d sign ->
-         if mem_named_context (NamedDecl.get_id d) global_named_context then sign
+         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
 	 else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index bd92e9794..8e7f4613c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -181,10 +181,10 @@ let introduction ?(check=true) id =
     let gl = Proofview.Goal.assume gl in
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
-    let hyps = Proofview.Goal.hyps gl in
+    let hyps = named_context_val (Proofview.Goal.env gl) in
     let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
-    let () = if check && mem_named_context id hyps then
+    let () = if check && mem_named_context_val id hyps then
       user_err ~hdr:"Tactics.introduction"
         (str "Variable " ++ pr_id id ++ str " is already declared.")
     in
@@ -520,7 +520,7 @@ let mutual_fix f n rest j = Proofview.Goal.nf_enter { enter = begin fun gl ->
     let (sp', u')  = check_mutind env sigma n ar in
     if not (eq_mind sp sp') then
       error "Fixpoints should be on the same mutual inductive declaration.";
-    if mem_named_context f (named_context_of_val sign) then
+    if mem_named_context_val f sign then
       user_err ~hdr:"Logic.prim_refiner"
         (str "Name " ++ pr_id f ++ str " already used in the environment");
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
@@ -573,7 +573,7 @@ let mutual_cofix f others j = Proofview.Goal.nf_enter { enter = begin fun gl ->
   | [] -> sign
   | (f, ar) :: oth ->
     let open Context.Named.Declaration in
-    if mem_named_context f (named_context_of_val sign) then
+    if mem_named_context_val f sign then
       error "Name already used in the environment.";
     mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth
   in
@@ -2791,7 +2791,7 @@ let old_generalize_dep ?(with_let=false) c gl =
   let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
   let tothin' =
     match kind_of_term c with
-      | Var id when mem_named_context id sign && not (Id.List.mem id init_ids)
+      | Var id when mem_named_context_val id (val_of_named_context sign) && not (Id.List.mem id init_ids)
 	  -> id::tothin
       | _ -> tothin
   in
@@ -2945,8 +2945,8 @@ let unfold_body x =
   let open Context.Named.Declaration in
   Proofview.Goal.enter { enter = begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
-  let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let xval = match Context.Named.lookup x hyps with
+  let env = Proofview.Goal.env (Proofview.Goal.assume gl) in
+  let xval = match Environ.lookup_named x env with
   | LocalAssum _ -> user_err ~hdr:"unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
   | LocalDef (_,xval,_) -> xval
@@ -4364,7 +4364,7 @@ let induction_gen clear_flag isrec with_evars elim
   let cls = Option.default allHypsAndConcl cls in
   let t = typ_of env sigma c in
   let is_arg_pure_hyp =
-    isVar c && not (mem_named_context (destVar c) (Global.named_context()))
+    isVar c && not (mem_named_context_val (destVar c) (Global.named_context_val ()))
     && lbind == NoBindings && not with_evars && Option.is_empty eqname
     && clear_flag == None
     && has_generic_occurrences_but_goal cls (destVar c) env ccl in
@@ -4411,7 +4411,7 @@ let induction_gen_l isrec with_evars elim names lc =
       | [] -> Proofview.tclUNIT ()
       | c::l' ->
 	  match kind_of_term c with
-	    | Var id when not (mem_named_context id (Global.named_context()))
+	    | Var id when not (mem_named_context_val id (Global.named_context_val ()))
 		&& not with_evars ->
 		let _ = newlc:= id::!newlc in
 		atomize_list l'
@@ -4831,7 +4831,7 @@ let abstract_subproof id gk tac =
   let open Proofview.Notations in
   Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
   let sigma = Proofview.Goal.sigma gl in
-  let current_sign = Global.named_context()
+  let current_sign = Global.named_context_val ()
   and global_sign = Proofview.Goal.hyps gl in
   let sigma = Sigma.to_evar_map sigma in
   let evdref = ref sigma in
@@ -4839,8 +4839,8 @@ let abstract_subproof id gk tac =
     List.fold_right
       (fun d (s1,s2) ->
         let id = NamedDecl.get_id d in
-	if mem_named_context id current_sign &&
-          interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
+	if mem_named_context_val id current_sign &&
+          interpretable_as_section_decl evdref (lookup_named_val id current_sign) d
         then (s1,push_named_context_val d s2)
 	else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, empty_named_context_val) in