* http://cs.unibo.it/helm/.
*)
-(* mk_fresh_name context name typ *)
-(* returns an identifier which is fresh in the context *)
-(* and that resembles [name] as much as possible. *)
-(* [typ] will be the type of the variable *)
-let mk_fresh_name context name ~typ =
- let module C = Cic in
- let basename =
- match name with
- C.Anonymous ->
- (*CSC: great space for improvements here *)
- (try
- (match CicTypeChecker.type_of_aux' [] context typ with
- C.Sort C.Prop -> "H"
- | C.Sort C.CProp -> "H"
- | C.Sort C.Set -> "x"
- | _ -> "H"
- )
- with CicTypeChecker.TypeCheckerFailure _ -> "H"
- )
- | C.Name name ->
- Str.global_replace (Str.regexp "[0-9]*$") "" name
- in
- let already_used name =
- List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
- in
- if not (already_used basename) then
- C.Name basename
- else
- let rec try_next n =
- let name' = basename ^ string_of_int n in
- if already_used name' then
- try_next (n+1)
- else
- C.Name name'
- in
- try_next 1
-;;
-
let new_meta_of_proof ~proof:(_, metasenv, _, _) =
CicMkImplicit.new_meta metasenv
) metasenv'
in
let bo' = subst_in bo in
- let newproof = uri,metasenv'',bo',ty in
+ (* Metavariables can appear also in the *statement* of the theorem
+ * since the parser does not reject as statements terms with
+ * metavariable therein *)
+ let ty' = subst_in ty in
+ let newproof = uri,metasenv'',bo',ty' in
(newproof, metasenv'')
(*CSC: commento vecchio *)
let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
let (uri,_,bo,ty) = proof in
let bo' = subst_in bo in
+ (* Metavariables can appear also in the *statement* of the theorem
+ * since the parser does not reject as statements terms with
+ * metavariable therein *)
+ let ty' = subst_in ty in
let metasenv' =
List.fold_right
(fun metasenv_entry i ->
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty in
+ let newproof = uri,metasenv',bo',ty' in
(newproof, metasenv')