diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 4 | ||||
| -rw-r--r-- | proofs/logic.ml | 6 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 2 | ||||
| -rw-r--r-- | proofs/refiner.ml | 6 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 4 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 2 |
8 files changed, 13 insertions, 15 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 33a86402ef..d6ed201d84 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -157,7 +157,7 @@ let error_incompatible_inst clenv mv = (str "An incompatible instantiation has already been found for " ++ pr_id id) | _ -> - anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned") + anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.") (* TODO: replace by clenv_unify (mkMeta mv) rhs ? *) let clenv_assign mv rhs clenv = @@ -433,7 +433,7 @@ let explain_no_such_bound_variable evd id = | Cltyp (na, _) -> na | Clval (na, _, _) -> na in - if na != Anonymous then out_name na :: l else l + if na != Anonymous then Name.get_id na :: l else l in let mvl = List.fold_left fold [] (Evd.meta_list evd) in user_err ~hdr:"Evd.meta_with_name" diff --git a/proofs/logic.ml b/proofs/logic.ml index cd2cfbd32f..c329bdf4aa 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -414,7 +414,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = | _ -> if occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refiner called with a meta in non app/case subterm"); + anomaly (Pp.str "refiner called with a meta in non app/case subterm."); let (sigma, t'ty) = goal_type_of env sigma trm in let sigma = check_conv_leq_goal env sigma trm t'ty conclty in (goalacc,t'ty,sigma, trm) @@ -474,7 +474,7 @@ and mk_hdgoals sigma goal goalacc trm = | _ -> if !check && occur_meta sigma (EConstr.of_constr trm) then - anomaly (Pp.str "refine called with a dependent meta"); + anomaly (Pp.str "refine called with a dependent meta."); let (sigma, ty) = goal_type_of env sigma trm in goalacc, ty, sigma, trm @@ -502,7 +502,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let ((ind, u), spec) = try Tacred.find_hnf_rectype env sigma ct - with Not_found -> anomaly (Pp.str "mk_casegoals") in + with Not_found -> anomaly (Pp.str "mk_casegoals.") in let indspec = ((ind, EConstr.EInstance.kind sigma u), spec) in let (lbrty,conclty) = type_case_branches_with_names env sigma indspec p c in (acc'',lbrty,conclty,sigma,p',c') diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index aaceb7b762..3fb66d1b87 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -113,7 +113,7 @@ let get_current_context () = let current_proof_statement () = match Proof_global.V82.get_current_initial_conclusions () with | (id,([concl],strength)) -> id,strength,concl - | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement") + | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.") let solve ?with_end_tac gi info_lvl tac pr = try diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4d2f534a76..5ec34a6387 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -719,7 +719,7 @@ type state = pstate list let freeze ~marshallable = match marshallable with | `Yes -> - CErrors.anomaly (Pp.str"full marshalling of proof state not supported") + CErrors.anomaly (Pp.str"full marshalling of proof state not supported.") | `Shallow -> !pstates | `No -> !pstates let unfreeze s = pstates := s; update_proof_mode () diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 7cd526843a..383a6a5233 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -195,7 +195,7 @@ let decl_red_expr s e = end let out_arg = function - | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable") + | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.") | ArgArg x -> x let out_with_occurrences (occs,c) = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 259e96a276..91e6dc4ab2 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -188,8 +188,6 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) (fun hypl -> List.subtract cmp hypl oldhyps) hyps in - let emacs_str s = - if !Flags.print_emacs then s else "" in let s = let frst = ref true in List.fold_left @@ -199,9 +197,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) "" lh)) "" newhyps in Feedback.msg_notice - (str (emacs_str "<infoH>") + (str "<infoH>" ++ (hov 0 (str s)) - ++ (str (emacs_str "</infoH>"))); + ++ (str "</infoH>")); tclIDTAC goal;; diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 97c5cda770..66d91c634a 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -75,7 +75,7 @@ let pf_get_new_ids ids gls = (fun id acc -> (next_ident_away id (acc@avoid))::acc) ids [] -let pf_global gls id = EConstr.of_constr (Constrintern.construct_reference (pf_hyps gls) id) +let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id)) let pf_reduction_of_red_expr gls re c = let (redfun, _) = reduction_of_red_expr (pf_env gls) re in @@ -171,7 +171,7 @@ module New = struct (** We only check for the existence of an [id] in [hyps] *) let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in - EConstr.of_constr (Constrintern.construct_reference hyps id) + Constrintern.construct_reference hyps id let pf_env = Proofview.Goal.env let pf_concl = Proofview.Goal.concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e6e60e27f7..1172e55ac6 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -100,7 +100,7 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> ('b, 'r) Proofview.Goal.t -> 'a - val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> constr + val pf_global : identifier -> ('a, 'r) Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a |