let rec debug_aux t i =
let module C = Cic in
let module U = UriManager in
- CicPp.ppobj (C.Variable ("DEBUG", None,
- C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
- C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
- C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
- C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
- C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
- C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
- C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
- C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
- C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
- t
- )
- )
- )
- )
- )
- )
- )
- )
- )
- )) ^ "\n" ^ i
+ CicPp.ppobj (C.Variable ("DEBUG", None, t)) ^ "\n" ^ i
in
if !fdebug = 0 then
begin
let module S = CicSubstitution in
function
C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
- | C.Var _ as t -> if l = [] then t else C.Appl (t::l)
+ | C.Var uri as t ->
+ (match CicEnvironment.get_cooked_obj uri 0 with
+ C.Definition _ -> raise ReferenceToDefinition
+ | C.Axiom _ -> raise ReferenceToAxiom
+ | C.CurrentProof _ -> raise ReferenceToCurrentProof
+ | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+ | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
+ | C.Variable (_,Some body,_) -> whdaux l body
+ )
| C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
| C.Sort _ as t -> t (* l should be empty *)
| C.Implicit as t -> t
(match CicEnvironment.get_cooked_obj uri cookingsno with
C.Definition (_,body,_,_) -> whdaux l body
| C.Axiom _ -> if l = [] then t else C.Appl (t::l)
- (*CSC: Prossima riga sbagliata: Var punta alle variabili, non Const *)
- | C.Variable _ -> if l = [] then t else C.Appl (t::l)
+ | C.Variable _ -> raise ReferenceToVariable
| C.CurrentProof (_,_,body,_) -> whdaux l body
| C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
)
let t1' = whd t1
and t2' = whd t2 in
debug t1' [t2'] "POSTWHD";
- (*if !fdebug = 0 then ignore(Unix.system "read" );*)
match (t1',t2') with
(C.Rel n1, C.Rel n2) -> n1 = n2
| (C.Var uri1, C.Var uri2) -> U.eq uri1 uri2