X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicElim.ml;h=e3fca907dd562f494a479333400c33ef069f08b8;hb=e6b28085c97ae7b9bd3f3262b105f6b84f42b047;hp=ab7ddd0e1fb2bb0a75bd4a4a48a3a82ae12f5f37;hpb=ce2fd238ae65537f65067d402482adb1874176db;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicElim.ml b/helm/ocaml/cic_proof_checking/cicElim.ml index ab7ddd0e1..e3fca907d 100644 --- a/helm/ocaml/cic_proof_checking/cicElim.ml +++ b/helm/ocaml/cic_proof_checking/cicElim.ml @@ -29,12 +29,14 @@ exception Elim_failure of string exception Can_t_eliminate let debug_print = fun _ -> () +(*let debug_print = prerr_endline *) let counter = ref ~-1 ;; -let fresh_binder () = +let fresh_binder () = Cic.Name "matita_dummy" +(* incr counter; - Cic.Name ("e" ^ string_of_int !counter) + Cic.Name ("e" ^ string_of_int !counter) *) (** verifies if a given inductive type occurs in a term in target position *) let rec recursive uri typeno = function @@ -367,6 +369,14 @@ let elim_of ?(sort = Cic.Type (CicUniv.fresh ())) uri typeno = (* debug_print (CicPp.ppterm eliminator_type); debug_print (CicPp.ppterm eliminator_body); +*) + let eliminator_type = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_type in + let eliminator_body = + FreshNamesGenerator.mk_fresh_names [] [] [] eliminator_body in +(* +debug_print (CicPp.ppterm eliminator_type); +debug_print (CicPp.ppterm eliminator_body); *) let (computed_type, ugraph) = try