diff options
Diffstat (limited to 'ide/coqide/idetop.ml')
| -rw-r--r-- | ide/coqide/idetop.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index 297dc3a706..602acefa7c 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -195,7 +195,7 @@ let concl_next_tac = let process_goal sigma g = let env = Goal.V82.env sigma g in let min_env = Environ.reset_context env in - let id = Goal.uid g in + let id = if Printer.print_goal_names () then Names.Id.to_string (Termops.evar_suggested_name g sigma) else "" in let ccl = pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g) in @@ -206,7 +206,7 @@ let process_goal sigma g = let (_env, hyps) = Context.Compacted.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in - { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id } let process_goal_diffs diff_goal_map oldp nsigma ng = let open Evd in @@ -317,7 +317,7 @@ let pattern_of_string ?env s = | None -> Global.env () | Some e -> e in - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in + let constr = Pcoq.parse_string Pcoq.Constr.cpattern s in let (_, pat) = Constrintern.intern_constr_pattern env (Evd.from_env env) constr in pat |