diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 8b48655940..08354ef556 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -307,6 +307,17 @@ let rename_hyp id1 id2 sign = (fun (_,b,t) _ -> (id2,b,t)) (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) +(**********************************************************************) + +let name_prop_vars env sigma ctxt = + List.map2 (fun (na,b,t as d) s -> + if na = Anonymous && s = prop_sort then + let s = match Namegen.head_name t with Some id -> string_of_id id | None -> "" in + (Name (add_suffix (id_of_string "H") s),b,t) + else + d) + ctxt (sorts_of_context env sigma ctxt) + (************************************************************************) (************************************************************************) (* Implementation of the logical rules *) @@ -511,7 +522,7 @@ and mk_casegoals sigma goal goalacc p c = try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly (Pp.str "mk_casegoals") in let (lbrty,conclty) = - type_case_branches_with_names env indspec p c in + type_case_branches_with_names (name_prop_vars env sigma) env indspec p c in (acc'',lbrty,conclty,sigma,p',c') |