diff options
| -rw-r--r-- | pretyping/cases.ml | 11 | ||||
| -rw-r--r-- | tactics/tactics.ml | 19 | ||||
| -rw-r--r-- | toplevel/class.ml | 11 |
3 files changed, 32 insertions, 9 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ff0ccd21a8..52c8ca4198 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -561,12 +561,13 @@ let dependencies_in_pure_rhs nargs eqns = let deps_columns = matrix_transpose deps_rows in List.map (List.exists ((=) true)) deps_columns -let dependent_in_decl b d = - fold_rel_declaration (fun c -> (||) (dependent b c)) d false +let dependent_decl a = function + | (na,None,t) -> dependent a t + | (na,Some c,t) -> dependent a t || dependent a c let rec dep_in_tomatch n = function | (Pushed _ | Alias _) :: l -> dep_in_tomatch n l - | Abstract d :: l -> dependent_in_decl (mkRel n) d or dep_in_tomatch (n+1) l + | Abstract d :: l -> dependent_decl (mkRel n) d or dep_in_tomatch (n+1) l | [] -> false let dependencies_in_rhs nargs current tms eqns = @@ -574,10 +575,6 @@ let dependencies_in_rhs nargs current tms eqns = | Rel n when dep_in_tomatch n tms -> list_make nargs true | _ -> dependencies_in_pure_rhs nargs eqns -let dependent_decl a = function - | (na,None,t) -> dependent a t - | (na,Some c,t) -> dependent a t || dependent a c - (* Computing the matrix of dependencies *) (* We are in context d1...dn |- and [find_dependencies k 1 nextlist] diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 905511b120..c992fcc2ab 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2885,6 +2885,24 @@ let tclABSTRACT name_op tac gl = let admit_as_an_axiom gl = + let ccl = pf_concl gl in + let ids_of_sign = pf_ids_of_hyps gl in + let vars = global_vars_set (Global.env ()) ccl in + let sign = List.filter (fun (id,_,_) -> Idset.mem id vars) (pf_hyps gl) in + let name = add_suffix (get_current_proof_name ()) "_admitted" in + let na = next_global_ident_away false name ids_of_sign in + let concl = it_mkNamedProd_or_LetIn ccl sign in + if occur_existential concl then error "\"admit\" cannot handle existentials"; + let axiom = + let cd = Entries.ParameterEntry (concl,false) in + let con = Declare.declare_internal_constant na (cd,IsAssumption Logical) in + constr_of_global (ConstRef con) + in + exact_no_check + (applist (axiom, + List.rev (Array.to_list (instance_from_named_context sign)))) + gl +(* let current_sign = Global.named_context() and global_sign = pf_hyps gl in let sign,secsign = @@ -2908,3 +2926,4 @@ let admit_as_an_axiom gl = (applist (axiom, List.rev (Array.to_list (instance_from_named_context sign)))) gl +*) diff --git a/toplevel/class.ml b/toplevel/class.ml index 7e5fc1297a..5e0713ea9d 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -178,6 +178,13 @@ let get_strength stre ref cls clt = let stref = strength_of_global ref in strength_min [stre;stres;stret;stref] +let ident_key_of_class = function + | CL_FUN -> "Funclass" + | CL_SORT -> "Sortclass" + | CL_CONST sp -> string_of_label (con_label sp) + | CL_IND (sp,_) -> string_of_label (label sp) + | CL_SECVAR id -> string_of_id id + (* coercion identité *) let error_not_transparent source = @@ -218,8 +225,8 @@ let build_id_coercion idf_opt source = match idf_opt with | Some idf -> idf | None -> - id_of_string ("Id_"^(string_of_class source)^"_"^ - (string_of_class (fst (find_class_type t)))) + id_of_string ("Id_"^(ident_key_of_class source)^"_"^ + (ident_key_of_class (fst (find_class_type t)))) in let constr_entry = (* Cast is necessary to express [val_f] is identity *) DefinitionEntry |