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 /plugins/decl_mode | |
| 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 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 6 | ||||
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 4 | ||||
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 2 |
4 files changed, 8 insertions, 6 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index e0aee15e60..541b599209 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -316,7 +316,7 @@ let rec match_aliases names constr = function let args,bnames,body = match_aliases qnames body q in st::args,bnames,body -let detype_ground c = Detyping.detype false [] [] c +let detype_ground c = Detyping.detype false [] [] Evd.empty c let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = let et,pinfo = diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index b5566127f1..c5a474d39f 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -1034,12 +1034,12 @@ let thesis_for obj typ per_info env= let ind,u = destInd cind in let _ = if not (eq_ind ind per_info.per_ind) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" - ((Printer.pr_constr_env env obj) ++ spc () ++ + ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++ str "cannot give an induction hypothesis (wrong parameters).") in let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in compose_prod rc (Reductionops.whd_beta Evd.empty hd2) @@ -1273,7 +1273,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let understand_my_constr c gls = let env = pf_env gls in let nc = names_of_rel_context env in - let rawc = Detyping.detype false [] nc c in + let rawc = Detyping.detype false [] nc Evd.empty c in let rec frob = function | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None) | rc -> map_glob_constr frob rc diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index a930245b65..9d909fda30 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -26,8 +26,8 @@ let pr_goal gs = let preamb,thesis,penv,pc = (str " *** Declarative Mode ***" ++ fnl ()++fnl ()), (str "thesis := " ++ fnl ()), - Printer.pr_context_of env, - Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g) + Printer.pr_context_of env sigma, + Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in preamb ++ str" " ++ hv 0 (penv ++ fnl () ++ diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 7f63c4200d..be2e44cff6 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -20,6 +20,8 @@ let pr_label = function Anonymous -> mt () | Name id -> pr_id id ++ spc () ++ str ":" ++ spc () +let pr_constr env c = pr_constr env Evd.empty c + let pr_justification_items env = function Some [] -> mt () | Some (_::_ as l) -> |