← Back to branch summary

~naesten/coq/trunk

« back to all changes in this revision

Viewing changes to plugins/funind/functional_principles_types.ml

  • Committer: herbelin
  • Date: 2009-11-09 18:05:13 UTC
  • Revision ID: svn-v4:85f007b7-540e-0410-9357-904b9bb8a0f7:trunk:12485
A bit of cleaning around name generation + creation of dedicated file namegen.ml

Show diffs side-by-side

added added

removed removed

Lines of Context:
plugins/funind/functional_principles_types.ml
2
2
open Util
3
3
open Term
4
4
open Termops
 
5
open Namegen
5
6
open Names
6
7
open Declarations
7
8
open Pp
67
68
    match predicates with
68
69
    | [] -> []
69
70
    |(Name x,v,t)::predicates ->
70
 
       let id =  Nameops.next_ident_away x avoid in
 
71
       let id =  Namegen.next_ident_away x avoid in
71
72
       Hashtbl.add tbl id x;
72
73
       (Name id,v,t)::(change_predicates_names (id::avoid) predicates)
73
74
    | (Anonymous,_,_)::_ -> anomaly "Anonymous property binder "
330
331
  (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
331
332
     observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
332
333
  let new_princ_name =
333
 
    next_global_ident_away true (id_of_string "___________princ_________") []
 
334
    next_ident_away_in_goal (id_of_string "___________princ_________") []
334
335
  in
335
336
  begin
336
337
    Lemmas.start_proof