diff options
| -rw-r--r-- | contrib/interface/centaur.ml | 10 | ||||
| -rw-r--r-- | contrib/interface/showproof_ct.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/translate.ml | 8 | ||||
| -rw-r--r-- | contrib/interface/translate.mli | 4 |
4 files changed, 13 insertions, 11 deletions
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml index fd60e1e61f..1cd2070479 100644 --- a/contrib/interface/centaur.ml +++ b/contrib/interface/centaur.ml @@ -252,7 +252,7 @@ let add_search (global_reference:global_reference) assumptions cstr = global_reference) in let ast = try - CT_premise (CT_ident id_string, translate_constr assumptions cstr) + CT_premise (CT_ident id_string, translate_constr false assumptions cstr) with Not_found -> CT_premise (CT_ident id_string, CT_coerce_ID_to_FORMULA( @@ -271,14 +271,14 @@ let ctf_EmptyGoalMessage id = let print_check (ast, judg) = let {uj_val=value; uj_type=typ} = judg in let value_ct_ast = - (try translate_constr (Global.env()) value + (try translate_constr false (Global.env()) value with UserError(f,str) -> raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) value) ++ fnl () ++ str ))) in let type_ct_ast = - (try translate_constr (Global.env()) typ + (try translate_constr false (Global.env()) typ with UserError(f,str) -> raise(UserError(f, Ast.print_ast (ast_of_constr true (Global.env()) value) ++ fnl() ++ str))) in @@ -300,8 +300,8 @@ and ntyp = nf_betaiota typ in (CT_premises_list [CT_eval_result (xlate_formula ast, - translate_constr env nvalue, - translate_constr env ntyp)]))));; + translate_constr false env nvalue, + translate_constr false env ntyp)]))));; diff --git a/contrib/interface/showproof_ct.ml b/contrib/interface/showproof_ct.ml index b689620e34..ee901c5e7c 100644 --- a/contrib/interface/showproof_ct.ml +++ b/contrib/interface/showproof_ct.ml @@ -52,7 +52,7 @@ let stde() = (Global.env()) ;; let spt t = - let f = (translate_constr (stde()) t) in + let f = (translate_constr true (stde()) t) in Hashtbl.add ct_FORMULA_constr f t; CT_text_formula f ;; diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml index c691ff912e..9d4d628044 100644 --- a/contrib/interface/translate.ml +++ b/contrib/interface/translate.ml @@ -108,8 +108,8 @@ let rec discard_coercions = | it -> it;; (*translates a formula into a centaur-tree --> FORMULA *) -let translate_constr assumptions c = - let com = ast_of_constr true assumptions c in +let translate_constr at_top assumptions c = + let com = ast_of_constr at_top assumptions c in (* dead code: let rcom = relativize_cci (discard_coercions com) in *) xlate_formula (Ctast.ast_to_ct com) (* dead code: rcom *);; @@ -119,7 +119,7 @@ let translate_sign env = let l = fold_named_context (fun env (id,v,c) l -> - (CT_premise(CT_ident(string_of_id id), translate_constr env c))::l) + (CT_premise(CT_ident(string_of_id id), translate_constr false env c))::l) env ~init:[] in CT_premises_list l;; @@ -158,4 +158,4 @@ let translate_path l = (*translates a path and a goal into a centaur-tree --> RULE *) let translate_goal (g:goal) = - CT_rule(translate_sign (evar_env g), translate_constr (evar_env g) g.evar_concl);; + CT_rule(translate_sign (evar_env g), translate_constr true (evar_env g) g.evar_concl);; diff --git a/contrib/interface/translate.mli b/contrib/interface/translate.mli index 46d785f4bf..65d8331b2d 100644 --- a/contrib/interface/translate.mli +++ b/contrib/interface/translate.mli @@ -5,5 +5,7 @@ open Environ;; open Term;; val translate_goal : goal -> ct_RULE;; -val translate_constr : env -> constr -> ct_FORMULA;; +(* The boolean argument indicates whether names from the environment should *) +(* be avoided (same interpretation as for prterm_env and ast_of_constr) *) +val translate_constr : bool -> env -> constr -> ct_FORMULA;; val translate_path : int list -> ct_SIGNED_INT_LIST;; |