diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0f81943e2..8b3e11848 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -871,13 +871,14 @@ let vernac_set_end_tac tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) let vernac_set_used_variables e = + let open Context.Named.Declaration in let env = Global.env () in let tys = List.map snd (Proof.initial_goals (Proof_global.give_me_the_proof ())) in let l = Proof_using.process_expr env e tys in let vars = Environ.named_context env in List.iter (fun id -> - if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then + if not (List.exists (Id.equal id % get_id) vars) then errorlabstrm "vernac_set_used_variables" (str "Unknown variable: " ++ pr_id id)) l; @@ -1568,6 +1569,7 @@ exception NoHyp We only print the type and a small statement to this comes from the goal. Precondition: there must be at least one current goal. *) let print_about_hyp_globs ref_or_by_not glnumopt = + let open Context.Named.Declaration in try let gl,id = match glnumopt,ref_or_by_not with @@ -1580,11 +1582,11 @@ let print_about_hyp_globs ref_or_by_not glnumopt = (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in - let (id,bdyopt,typ) = Context.Named.lookup id hyps in - let natureofid = match bdyopt with - | None -> "Hypothesis" - | Some bdy ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_constr typ ++ fnl() ++ fnl() + let decl = Context.Named.lookup id hyps in + let natureofid = match decl with + | LocalAssum _ -> "Hypothesis" + | LocalDef (_,bdy,_) ->"Constant (let in)" in + v 0 (pr_id id ++ str":" ++ pr_constr (get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not |