diff options
| -rw-r--r-- | engine/evd.mli | 2 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 14 | ||||
| -rw-r--r-- | kernel/typeops.ml | 10 | ||||
| -rw-r--r-- | kernel/typeops.mli | 8 | ||||
| -rw-r--r-- | man/coqdep.1 | 2 | ||||
| -rw-r--r-- | pretyping/nativenorm.ml | 50 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_bullet.ml | 40 | ||||
| -rw-r--r-- | tactics/tactics.ml | 10 |
9 files changed, 44 insertions, 93 deletions
diff --git a/engine/evd.mli b/engine/evd.mli index 9055dcc86..96e4b6acc 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -31,7 +31,7 @@ open Environ (** {6 Evars} *) type evar = existential_key -(** Existential variables. TODO: Should be made opaque one day. *) +(** Existential variables. *) val string_of_existential : evar -> string diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index d2b41aae9..8568bf14b 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -166,16 +166,10 @@ let rec check_with_mod env struc (idl,mp1) mp equiv = let mb_mp1 = lookup_module mp1 env in let mtb_mp1 = module_type_of_module mb_mp1 in let cst = match old.mod_expr with - | Abstract -> - begin - try - let mtb_old = module_type_of_module old in - let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in - Univ.ContextSet.add_constraints chk_cst old.mod_constraints - with Failure _ -> - (* TODO: where can a Failure come from ??? *) - error_incorrect_with_constraint lab - end + | Abstract -> + let mtb_old = module_type_of_module old in + let chk_cst = Subtyping.check_subtypes env' mtb_mp1 mtb_old in + Univ.ContextSet.add_constraints chk_cst old.mod_constraints | Algebraic (NoFunctor (MEident(mp'))) -> check_modpath_equiv env' mp1 mp'; old.mod_constraints diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 044877e82..b40badd7c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -65,6 +65,10 @@ let type_of_type u = let uu = Universe.super u in mkType uu +let type_of_sort = function + | Prop c -> type1 + | Type u -> type_of_type u + (*s Type of a de Bruijn index. *) let type_of_relative env n = @@ -323,11 +327,7 @@ let rec execute env cstr = let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) - | Sort (Prop c) -> - type1 - - | Sort (Type u) -> - type_of_type u + | Sort s -> type_of_sort s | Rel n -> type_of_relative env n diff --git a/kernel/typeops.mli b/kernel/typeops.mli index a8f7fba9a..96be6c14a 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -37,15 +37,19 @@ val assumption_of_judgment : env -> unsafe_judgment -> types val type_judgment : env -> unsafe_judgment -> unsafe_type_judgment (** {6 Type of sorts. } *) +val type1 : types +val type_of_sort : Sorts.t -> types val judge_of_prop : unsafe_judgment val judge_of_set : unsafe_judgment val judge_of_prop_contents : contents -> unsafe_judgment val judge_of_type : universe -> unsafe_judgment (** {6 Type of a bound variable. } *) +val type_of_relative : env -> int -> types val judge_of_relative : env -> int -> unsafe_judgment (** {6 Type of variables } *) +val type_of_variable : env -> variable -> types val judge_of_variable : env -> variable -> unsafe_judgment (** {6 type of a constant } *) @@ -66,9 +70,9 @@ val judge_of_abstraction : env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment -val sort_of_product : env -> sorts -> sorts -> sorts - (** {6 Type of a product. } *) +val sort_of_product : env -> sorts -> sorts -> sorts +val type_of_product : env -> Name.t -> sorts -> sorts -> types val judge_of_product : env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment diff --git a/man/coqdep.1 b/man/coqdep.1 index 81f7e1e0d..ed727db7c 100644 --- a/man/coqdep.1 +++ b/man/coqdep.1 @@ -82,7 +82,7 @@ Prints the dependencies of Caml modules. \" the standard output. No dependency is computed with this option. .TP .BI \-I/\-Q/\-R \ options -Have the same effects on load path and modules names than for other +Have the same effects on load path and modules names as for other coq commands (coqtop, coqc). .TP .BI \-coqlib \ directory diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 39c2ceeba..1038945c1 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -5,13 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open CErrors open Term open Vars open Environ open Reduction -open Univ open Declarations open Names open Inductive @@ -20,8 +18,6 @@ open Nativecode open Nativevalues open Context.Rel.Declaration -module RelDecl = Context.Rel.Declaration - (** This module implements normalization by evaluation to OCaml code *) exception Find_at of int @@ -177,44 +173,6 @@ let build_case_type dep p realargs c = if dep then mkApp(mkApp(p, realargs), [|c|]) else mkApp(p, realargs) -(* TODO move this function *) -let type_of_rel env n = - env |> lookup_rel n |> RelDecl.get_type |> lift n - -let type_of_prop = mkSort type1_sort - -let type_of_sort s = - match s with - | Prop _ -> type_of_prop - | Type u -> mkType (Univ.super u) - -let type_of_var env id = - let open Context.Named.Declaration in - try env |> lookup_named id |> get_type - with Not_found -> - anomaly ~label:"type_of_var" (str "variable " ++ Id.print id ++ str " unbound.") - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - if is_impredicative_set env then - (* Rule is (Type,Set,Set) in the Set-impredicative calculus *) - rangsort - else - (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *) - Type (sup u1 type0_univ) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (sup type0_univ u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (sup u1 u2) - (* normalisation of values *) let branch_of_switch lvl ans bs = @@ -328,15 +286,15 @@ and nf_atom_type env sigma atom = match atom with | Arel i -> let n = (nb_rel env - i) in - mkRel n, type_of_rel env n + mkRel n, Typeops.type_of_relative env n | Aconstant cst -> mkConstU cst, Typeops.type_of_constant_in env cst | Aind ind -> mkIndU ind, Inductiveops.type_of_inductive env ind | Asort s -> - mkSort s, type_of_sort s + mkSort s, Typeops.type_of_sort s | Avar id -> - mkVar id, type_of_var env id + mkVar id, Typeops.type_of_variable env id | Acase(ans,accu,p,bs) -> let a,ta = nf_accu_type env sigma accu in let ((mind,_),u as ind),allargs = find_rectype_a env ta in @@ -387,7 +345,7 @@ and nf_atom_type env sigma atom = let vn = mk_rel_accu (nb_rel env) in let env = push_rel (LocalAssum (n,dom)) env in let codom,s2 = nf_type_sort env sigma (codom vn) in - mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2) + mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2 | Aevar(ev,ty) -> let ty = nf_type env sigma ty in mkEvar ev, ty diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 079524f34..56f8b33e0 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -214,7 +214,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty = type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty | Const (cst, u) -> let t = constant_type_in env (cst, EInstance.kind sigma u) in - (* TODO *) sigma, EConstr.of_constr t | Var id -> sigma, type_of_var env id | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u)) diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index f80cb7cc6..4f575ab4b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -110,10 +110,6 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - (* Used only in the next function. - TODO: use a recursive function instead? *) - exception SuggestFound of t - let suggest_bullet (prf : proof): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) @@ -122,24 +118,24 @@ module Strict = struct | b::_ -> Unfinished b | _ -> NoBulletInUse else (* There is no goal under focus but some are unfocussed, - let us look at the bullet needed. If no *) - let pcobaye = ref prf in - try - while true do - let pcobaye', b = pop !pcobaye in - (* pop went well, this means that there are no more goals - *under this* bullet b, see if a new b can be pushed. *) - (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) - raise (SuggestFound b) - with SuggestFound _ as e -> raise e - | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) - pcobaye := pcobaye' - done; - assert false - with SuggestFound b -> Suggest b - | _ -> NeedClosingBrace (* No push was possible, but there are still - subgoals somewhere: there must be a "}" to use. *) - + let us look at the bullet needed. *) + let rec loop prf = + match pop prf with + | prf, b -> + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + begin + try ignore (push b prf); Suggest b + with _ -> + (* b could not be pushed, so we must look for a outer bullet *) + loop prf + end + | exception _ -> + (* No pop was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + NeedClosingBrace + in + loop prf let rec pop_until (prf : proof) bul : proof = let prf', b = pop prf in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d6c24e9cc..6f7e61f6b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1579,11 +1579,11 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in let indmv = destMeta sigma (nth_arg sigma i elimclause.templval.rebus) in let hypmv = - try match List.remove Int.equal indmv (clenv_independent elimclause) with - | [a] -> a - | _ -> failwith "" - with Failure _ -> user_err ~hdr:"elimination_clause" - (str "The type of elimination clause is not well-formed.") in + match List.remove Int.equal indmv (clenv_independent elimclause) with + | [a] -> a + | _ -> user_err ~hdr:"elimination_clause" + (str "The type of elimination clause is not well-formed.") + in let elimclause' = clenv_fchain ~flags indmv elimclause indclause in let hyp = mkVar id in let hyp_typ = Retyping.get_type_of env sigma hyp in |