diff options
| author | Hugo Herbelin | 2014-08-12 14:03:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-09-12 10:39:32 +0200 |
| commit | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (patch) | |
| tree | 32282ac2f1198738c8c545b19215ff0a0d9ef6ce /ide | |
| parent | b720cd3cbefa46da784b68a8e016a853f577800c (diff) | |
Referring to evars by names. Added a parser for evars (but parsing of
instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5e03d27732..61c60c02f2 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -122,7 +122,7 @@ let query (s,id) = Stm.query ~at:id s; read_stdout () let hyp_next_tac sigma env (id,_,ast) = let id_s = Names.Id.to_string id in - let type_s = string_of_ppcmds (pr_ltype_env env ast) in + let type_s = string_of_ppcmds (pr_ltype_env env sigma ast) in [ ("clear "^id_s),("clear "^id_s^"."); ("apply "^id_s),("apply "^id_s^"."); @@ -184,10 +184,10 @@ let process_goal sigma g = let id = Goal.uid g in let ccl = let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - string_of_ppcmds (pr_goal_concl_style_env env norm_constr) in + string_of_ppcmds (pr_goal_concl_style_env env sigma norm_constr) in let process_hyp d = let d = Context.map_named_list_declaration (Reductionops.nf_evar sigma) d in - (string_of_ppcmds (pr_var_list_decl min_env d)) in + (string_of_ppcmds (pr_var_list_decl min_env sigma d)) in let hyps = List.map process_hyp (compact_named_context (Environ.named_context env)) in { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } @@ -222,7 +222,7 @@ let evars () = let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in - let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar ev); } in + let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el with Proof_global.NoCurrentProof -> None |