diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/extraction/extraction.ml | 4 | ||||
| -rw-r--r-- | plugins/firstorder/formula.ml | 6 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/g_class.mlg | 13 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 3 | ||||
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 2 |
9 files changed, 26 insertions, 12 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 204f889f90..ef6c07bff2 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1044,7 +1044,9 @@ let fake_match_projection env p = let indu = mkIndU (ind,u) in let ctx, paramslet = let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((fst ind, mib.mind_ntypes - i - 1), u)) in - let rctx, _ = decompose_prod_assum (Vars.substl subst mip.mind_nf_lc.(0)) in + let (ctx, cty) = mip.mind_nf_lc.(0) in + let cty = Term.it_mkProd_or_LetIn cty ctx in + let rctx, _ = decompose_prod_assum (Vars.substl subst cty) in List.chop mip.mind_consnrealdecls.(0) rctx in let ci_pp_info = { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index a60a966cec..56b3dc97cf 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -13,7 +13,6 @@ open Names open Constr open EConstr open Vars -open Termops open Util open Declarations open Globnames @@ -100,9 +99,8 @@ let kind_of_formula env sigma term = else let has_realargs=(n>0) in let is_trivial= - let is_constant c = - Int.equal (nb_prod sigma (EConstr.of_constr c)) mib.mind_nparams in - Array.exists is_constant mip.mind_nf_lc in + let is_constant n = Int.equal n 0 in + Array.exists is_constant mip.mind_consnrealargs in if Inductiveops.mis_is_recursive (ind,mib,mip) || (has_realargs && not is_trivial) then diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..6fd2f7c2bc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg index 9ecc36bdf3..3f2fabeeee 100644 --- a/plugins/ltac/g_class.mlg +++ b/plugins/ltac/g_class.mlg @@ -99,8 +99,19 @@ TACTIC EXTEND is_ground | [ "is_ground" constr(ty) ] -> { is_ground ty } END +{ +let deprecated_autoapply_using = + CWarnings.create + ~name:"autoapply-using" ~category:"deprecated" + (fun () -> Pp.str "The syntax [autoapply ... using] is deprecated. Use [autoapply ... with] instead.") +} + TACTIC EXTEND autoapply -| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +| [ "autoapply" constr(c) "using" preident(i) ] -> { + deprecated_autoapply_using (); + autoapply c i + } +| [ "autoapply" constr(c) "with" preident(i) ] -> { autoapply c i } END { diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d833a2cde..e78d0f93a4 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -449,7 +449,7 @@ let evd_convertible env evd x y = unsolvable constraints remain, so we check that this unification does not introduce any new problem. *) let _, pbs = Evd.extract_all_conv_pbs evd in - let evd' = Evarconv.the_conv_x env x y evd in + let evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04..543d4de0fe 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 30f716d764..eac84f0543 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1766,7 +1766,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index a0b1d784f1..7216849948 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -209,7 +209,8 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac = let mind,indb = Inductive.lookup_mind_specif env (kn,i) in let tys = indb.Declarations.mind_nf_lc in let renamed_tys = - Array.mapi (fun j t -> + Array.mapi (fun j (ctx, cty) -> + let t = Term.it_mkProd_or_LetIn cty ctx in ppdebug(lazy Pp.(str "Search" ++ Printer.pr_constr_env env (project gl) t)); let t = Arguments_renaming.rename_type t (GlobRef.ConstructRef((kn,i),j+1)) in diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 552a4048b1..fb99b87108 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a = loop 0 let unif_HO env ise p c = - try Evarconv.the_conv_x env p c ise + try Evarconv.unify_delay env ise p c with Evarconv.UnableToUnify(ise, err) -> raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) |