diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 8 | ||||
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 6 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 12 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
6 files changed, 22 insertions, 16 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 0c8440fe5a..2241fb821c 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -175,6 +175,10 @@ and e_my_find_search db_list local_db hdc concl = in let tac_of_hint = fun (st, {pri = b; pat = p; code = t; poly = poly}) -> + let b = match Hints.repr_hint t with + | Unfold_nth _ -> 1 + | _ -> b + in (b, let tac = function | Res_pf (term,cl) -> unify_resolve poly st (term,cl) @@ -254,8 +258,8 @@ module SearchProblem = struct let d = s'.depth - s.depth in let d' = Int.compare s.priority s'.priority in let nbgoals s = List.length (sig_it s.tacres) in - if not (Int.equal d' 0) then d' - else if not (Int.equal d 0) then d + if not (Int.equal d 0) then d + else if not (Int.equal d' 0) then d' else Int.compare (nbgoals s) (nbgoals s') let branching s = diff --git a/tactics/equality.ml b/tactics/equality.ml index 7a8a3a97b3..89d14fdc7b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -918,7 +918,7 @@ let apply_on_clause (f,t) clause = (match kind_of_term (last_arg f_clause.templval.Evd.rebus) with | Meta mv -> mv | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in - clenv_fchain argmv f_clause clause + clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = let e = next_ident_away eq_baseid (ids_of_context env) in diff --git a/tactics/hints.ml b/tactics/hints.ml index 5630d20b5d..6250886821 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -677,7 +677,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) = match kind_of_term cty with | Prod _ -> failwith "make_exact_entry" | _ -> - let pat = pi3 (Patternops.pattern_of_constr env sigma cty) in + let pat = Patternops.pattern_of_constr env sigma cty in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_exact_entry" @@ -696,7 +696,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c, let sigma' = Evd.merge_context_set univ_flexible sigma ctx in let ce = mk_clenv_from_env env sigma' None (c,cty) in let c' = clenv_type (* ~reduce:false *) ce in - let pat = pi3 (Patternops.pattern_of_constr env ce.evd c') in + let pat = Patternops.pattern_of_constr env ce.evd c' in let hd = try head_pattern_bound pat with BoundPattern -> failwith "make_apply_entry" in @@ -794,7 +794,7 @@ let make_trivial env sigma poly ?(name=PathAny) r = let ce = mk_clenv_from_env env sigma None (c,t) in (Some hd, { pri=1; poly = poly; - pat = Some (pi3 (Patternops.pattern_of_constr env ce.evd (clenv_type ce))); + pat = Some (Patternops.pattern_of_constr env ce.evd (clenv_type ce)); name = name; code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) }) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 25d80b9c8e..2597606aa1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -689,12 +689,12 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = try Inl (coerce_to_evaluable_ref env x) with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in - Inr (pi3 (pattern_of_constr env sigma c)) in + Inr (pattern_of_constr env sigma c) in (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) with Not_found -> error_global_not_found_loc loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) - | Inr c -> Inr (pi3 (interp_typed_pattern ist env sigma c)) in + | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p let interp_constr_with_occurrences_and_name_as_list = @@ -1003,7 +1003,7 @@ let interp_induction_arg ist gl arg = try Sigma.here (constr_of_id env id', NoBindings) sigma with Not_found -> user_err_loc (loc, "interp_induction_arg", - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.") + pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") end }) in try @@ -1060,7 +1060,7 @@ let use_types = false let eval_pattern lfun ist env sigma ((glob,_),pat as c) = let bound_names = bound_glob_vars glob in if use_types then - (bound_names,pi3 (interp_typed_pattern ist env sigma c)) + (bound_names,interp_typed_pattern ist env sigma c) else (bound_names,instantiate_pattern env sigma lfun pat) @@ -2175,7 +2175,7 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in Proofview.V82.tactic begin fun gl -> - let (sigma,sign,op) = interp_typed_pattern ist env sigma op in + let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in let c_interp patvars = { Sigma.run = begin fun sigma -> let lfun' = Id.Map.fold (fun id c lfun -> @@ -2191,7 +2191,7 @@ and interp_atomic ist tac : unit Proofview.tactic = errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.") end } in (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl)) - { gl with sigma = sigma } + gl end end } end diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index f2e013641a..e181c8e14e 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -626,7 +626,7 @@ module New = struct errorlabstrm "Tacticals.general_elim_then_using" (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in - let elimclause' = clenv_fchain indmv elimclause indclause in + let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in let brnames = compute_induction_names (Array.length branchsigns) allnames in let flags = Unification.elim_flags () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c26ea56784..5cd17fad4c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1347,7 +1347,9 @@ let simplest_elim c = default_elim false None (c,NoBindings) *) let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause = - try clenv_fchain ~flags mv elimclause hypclause + (** The evarmap of elimclause is assumed to be an extension of hypclause, so + we do not need to merge the universes coming from hypclause. *) + try clenv_fchain ~with_univs:false ~flags mv elimclause hypclause with PretypeError (env,evd,NoOccurrenceFound (op,_)) -> (* Set the hypothesis name in the message *) raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id))) @@ -1634,7 +1636,7 @@ let progress_with_clause flags innerclause clause = let ordered_metas = List.rev (clenv_independent clause) in if List.is_empty ordered_metas then error "Statement without assumptions."; let f mv = - try Some (find_matching_clause (clenv_fchain mv ~flags clause) innerclause) + try Some (find_matching_clause (clenv_fchain ~with_univs:false mv ~flags clause) innerclause) with Failure _ -> None in try List.find_map f ordered_metas @@ -3809,7 +3811,7 @@ let recolle_clenv i params args elimclause gl = trying to unify (which would lead to trying to apply it to evars if y is a product). *) let indclause = mk_clenv_from_n gl (Some 0) (x,y) in - let elimclause' = clenv_fchain i acc indclause in + let elimclause' = clenv_fchain ~with_univs:false i acc indclause in elimclause') (List.rev clauses) elimclause |