aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml3
-rw-r--r--dev/ci/README.md5
-rw-r--r--engine/evarutil.mli8
-rw-r--r--engine/proofview.ml2
-rw-r--r--engine/termops.ml11
-rw-r--r--engine/termops.mli5
-rw-r--r--proofs/pfedit.ml3
-rw-r--r--proofs/proof_global.ml4
-rw-r--r--tactics/autorewrite.ml22
-rw-r--r--tactics/class_tactics.ml5
-rw-r--r--tactics/eqschemes.ml11
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml5
-rw-r--r--vernac/auto_ind_decl.ml17
-rw-r--r--vernac/comInductive.ml3
15 files changed, 57 insertions, 49 deletions
diff --git a/.travis.yml b/.travis.yml
index 5c7fc5a33..86a2aea66 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -82,9 +82,6 @@ matrix:
- TEST_TARGET="ci-coquelicot"
- if: NOT (type = pull_request)
env:
- - TEST_TARGET="ci-cross-crypto"
- - if: NOT (type = pull_request)
- env:
- TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi"
# ppx_tools_versioned requires a specific version findlib
- FINDLIB_VER=""
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 697a160ca..dc586c61f 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -89,6 +89,11 @@ We are currently running tests on the following platforms:
- AppVeyor is used to test the compilation of Coq and run the test-suite on
Windows.
+GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit
+message to bypass CI. Do not use this unless your commit only changes files
+that are not compiled (e.g. Markdown files like this one, or files under
+[`.github/`](/.github/)).
+
You can anticipate the results of most of these tests prior to submitting your
PR by running GitLab CI on your private branches. To do so follow these steps:
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index f271c14ea..f83f262b4 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -264,19 +264,19 @@ val e_new_evar :
?candidates:constr list -> ?store:Store.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode -> types -> constr
-[@@ocaml.deprecated "Use [Evd.new_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_evar]"]
val e_new_type_evar : env -> evar_map ref ->
?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
?naming:Misctypes.intro_pattern_naming_expr ->
?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
-[@@ocaml.deprecated "Use [Evd.new_type_evar]"]
+[@@ocaml.deprecated "Use [Evarutil.new_type_evar]"]
val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
-[@@ocaml.deprecated "Use [Evd.new_Type]"]
+[@@ocaml.deprecated "Use [Evarutil.new_Type]"]
val e_new_global : evar_map ref -> GlobRef.t -> constr
-[@@ocaml.deprecated "Use [Evd.new_global]"]
+[@@ocaml.deprecated "Use [Evarutil.new_global]"]
val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * UnivSubst.universe_opt_subst
[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/engine/proofview.ml b/engine/proofview.ml
index fdb0a215d..b4afb6415 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -39,7 +39,7 @@ let proofview p =
let compact el ({ solution } as pv) =
let nf c = Evarutil.nf_evar solution c in
- let nf0 c = EConstr.Unsafe.to_constr (Evarutil.nf_evar solution (EConstr.of_constr c)) in
+ let nf0 c = EConstr.(to_constr solution (of_constr c)) in
let size = Evd.fold (fun _ _ i -> i+1) solution 0 in
let new_el = List.map (fun (t,ty) -> nf t, nf ty) el in
let pruned_solution = Evd.drop_all_defined solution in
diff --git a/engine/termops.ml b/engine/termops.ml
index 0c567754a..eacc36107 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -781,24 +781,23 @@ let map_constr_with_full_binders sigma g f l cstr =
let fold_constr_with_full_binders sigma g f n acc c =
let open RelDecl in
- let inj c = EConstr.Unsafe.to_constr c in
match EConstr.kind sigma c with
| (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _
| Construct _) -> acc
| Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
- | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
+ | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
| App (c,l) -> Array.fold_left (f n) (f n acc c) l
| Proj (p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
| Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
| CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+ let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
diff --git a/engine/termops.mli b/engine/termops.mli
index 6e63539ca..255494031 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -75,8 +75,9 @@ val fold_constr_with_binders : Evd.evar_map ->
('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
val fold_constr_with_full_binders : Evd.evar_map ->
- (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
- 'a -> 'b -> constr -> 'b
+ (rel_declaration -> 'a -> 'a) ->
+ ('a -> 'b -> constr -> 'b) ->
+ 'a -> 'b -> constr -> 'b
val iter_constr_with_full_binders : Evd.evar_map ->
(rel_declaration -> 'a -> 'a) ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 03c0969fa..678c3ea3f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -200,8 +200,7 @@ let refine_by_tactic env sigma ty tac =
| [c, _] -> c
| _ -> assert false
in
- let ans = Reductionops.nf_evar sigma ans in
- let ans = EConstr.Unsafe.to_constr ans in
+ let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
(** [neff] contains the freshly generated side-effects *)
let neff = Evd.eval_side_effects sigma in
(** Reset the old side-effects *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3abdd129e..946379356 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -437,8 +437,8 @@ let return_proof ?(allow_partial=false) () =
(** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
- let proofs =
- List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
+ let proofs =
+ List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
proofs, Evd.evar_universe_context evd
let close_future_proof ~feedback_id proof =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0b0e629ab..c8fd0b7a7 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -228,7 +228,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
if metas then eqclause
else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
in
- let (equiv, args) = decompose_app (EConstr.Unsafe.to_constr (Clenv.clenv_type eqclause)) in
+ let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
@@ -236,17 +236,19 @@ let decompose_applied_relation metas env sigma c ctype left2right =
| _ -> raise Not_found
in
try
- let others,(c1,c2) = split_last_two args in
- let ty1, ty2 =
- Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c1), Typing.unsafe_type_of env eqclause.evd (EConstr.of_constr c2)
- in
- let ty = EConstr.Unsafe.to_constr ty in
- let ty1 = EConstr.Unsafe.to_constr ty1 in
+ let others,(c1,c2) = split_last_two args in
+ let ty1, ty2 = Typing.unsafe_type_of env eqclause.evd c1, Typing.unsafe_type_of env eqclause.evd c2 in
+ (* XXX: It looks like mk_clenv_from_env should be fixed instead? *)
+ let open EConstr in
+ let hyp_ty = Unsafe.to_constr ty in
+ let hyp_car = Unsafe.to_constr ty1 in
+ let hyp_prf = Unsafe.to_constr @@ Clenv.clenv_value eqclause in
+ let hyp_rel = Unsafe.to_constr @@ mkApp (equiv, Array.of_list others) in
+ let hyp_left = Unsafe.to_constr @@ c1 in
+ let hyp_right = Unsafe.to_constr @@ c2 in
(* if not (evd_convertible env eqclause.evd ty1 ty2) then None *)
(* else *)
- Some { hyp_cl=eqclause; hyp_prf=EConstr.Unsafe.to_constr (Clenv.clenv_value eqclause); hyp_ty = ty;
- hyp_car=ty1; hyp_rel=mkApp (equiv, Array.of_list others);
- hyp_l2r=left2right; hyp_left=c1; hyp_right=c2; }
+ Some { hyp_cl=eqclause; hyp_prf; hyp_ty; hyp_car; hyp_rel; hyp_l2r=left2right; hyp_left; hyp_right; }
with Not_found -> None
in
match find_rel ctype with
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index c105116ff..4beeaaae0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -1206,8 +1206,11 @@ let is_ground c =
let autoapply c i =
let open Proofview.Notations in
Proofview.Goal.enter begin fun gl ->
+ let hintdb = try Hints.searchtable_map i with Not_found ->
+ CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ "."))
+ in
let flags = auto_unif_flags Evar.Set.empty
- (Hints.Hint_db.transparent_state (Hints.searchtable_map i)) in
+ (Hints.Hint_db.transparent_state hintdb) in
let cty = Tacmach.New.pf_unsafe_type_of gl c in
let ce = mk_clenv_from gl (c,cty) in
unify_e_resolve false flags gl
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index eede13329..ad5239116 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -108,9 +108,14 @@ let get_coq_eq ctx =
user_err Pp.(str "eq not found.")
let univ_of_eq env eq =
- let eq = EConstr.of_constr eq in
- match Constr.kind (EConstr.Unsafe.to_constr (Retyping.get_type_of env (Evd.from_env env) eq)) with
- | Prod (_,t,_) -> (match Constr.kind t with Sort (Type u) -> u | _ -> assert false)
+ let open EConstr in
+ let eq = of_constr eq in
+ let sigma = Evd.from_env env in
+ match kind sigma (Retyping.get_type_of env sigma eq) with
+ | Prod (_,t,_) -> (match kind sigma t with
+ Sort k ->
+ (match ESorts.kind sigma k with Type u -> u | _ -> assert false)
+ | _ -> assert false)
| _ -> assert false
(**********************************************************************)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 339abbc2e..102b8e54d 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -293,7 +293,7 @@ let error_too_many_names pats =
str "Unexpected " ++
str (String.plural (List.length pats) "introduction pattern") ++
str ": " ++ pr_enum (Miscprint.pr_intro_pattern
- (fun c -> Printer.pr_constr_env env sigma (EConstr.Unsafe.to_constr (snd (c env (Evd.from_env env)))))) pats ++
+ (fun c -> Printer.pr_econstr_env env sigma (snd (c env (Evd.from_env env))))) pats ++
str ".")
let get_names (allow_conj,issimple) ({CAst.loc;v=pat} as x) = match pat with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index f47e6b2cd..10937322e 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,9 +232,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let c = fill_holes pfterm in
(* warning: side-effect on ownSign *)
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
- let invProof = EConstr.Unsafe.to_constr invProof in
- let p = Evarutil.nf_evars_universes sigma invProof in
- p, sigma
+ let p = EConstr.to_constr sigma invProof in
+ p, sigma
let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 30a268a11..8b56275c7 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -186,10 +186,10 @@ let build_beq_scheme mode kn =
*)
let compute_A_equality rel_list nlist eqA ndx t =
let lifti = ndx in
- let sigma = Evd.empty (** FIXME *) in
let rec aux c =
- let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
- match EConstr.kind sigma c with
+ let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in
+ let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in
+ match Constr.kind c with
| Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
| Var x ->
let eid = Id.of_string ("eq_"^(Id.to_string x)) in
@@ -198,7 +198,7 @@ let build_beq_scheme mode kn =
with Not_found -> raise (ParameterWithoutEquality (VarRef x))
in
mkVar eid, Safe_typing.empty_private_constants
- | Cast (x,_,_) -> aux (EConstr.applist (x,a))
+ | Cast (x,_,_) -> aux (Term.applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants
@@ -213,8 +213,8 @@ let build_beq_scheme mode kn =
List.fold_left Safe_typing.concat_private eff (List.rev effs)
in
let args =
- Array.append
- (Array.of_list (List.map (fun x -> lift lifti (EConstr.Unsafe.to_constr x)) a)) eqa in
+ Array.append
+ (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in
if Int.equal (Array.length args) 0 then eq, eff
else mkApp (eq, args), eff
with Not_found -> raise(EqNotFound (ind', fst ind))
@@ -224,10 +224,9 @@ let build_beq_scheme mode kn =
| Lambda _-> raise (EqUnknown "abstraction")
| LetIn _ -> raise (EqUnknown "let-in")
| Const (kn, u) ->
- let u = EConstr.EInstance.kind sigma u in
(match Environ.constant_opt_value_in env (kn, u) with
| None -> raise (ParameterWithoutEquality (ConstRef kn))
- | Some c -> aux (EConstr.applist (EConstr.of_constr c,a)))
+ | Some c -> aux (Term.applist (c,a)))
| Proj _ -> raise (EqUnknown "projection")
| Construct _ -> raise (EqUnknown "constructor")
| Case _ -> raise (EqUnknown "match")
@@ -271,7 +270,7 @@ let build_beq_scheme mode kn =
nparrec
(nparrec+3+2*nb_cstr_args)
(nb_cstr_args+ndx+1)
- (EConstr.of_constr cc)
+ cc
in
eff := Safe_typing.concat_private eff' !eff;
Array.set eqs ndx
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 101c14266..b93e8d9ac 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -27,7 +27,6 @@ open Impargs
open Reductionops
open Indtypes
open Pretyping
-open Evarutil
open Indschemes
open Context.Rel.Declaration
open Entries
@@ -158,7 +157,7 @@ let sign_level env evd sign =
| LocalDef _ -> lev, push_rel d env
| LocalAssum _ ->
let s = destSort (Reduction.whd_all env
- (EConstr.Unsafe.to_constr (nf_evar evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d))))))
+ (EConstr.to_constr evd (Retyping.get_type_of env evd (EConstr.of_constr (RelDecl.get_type d)))))
in
let u = univ_of_sort s in
(Univ.sup u lev, push_rel d env))
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 01:42:32 +0000