From 1633244fde7c007e23041b700da9d643596877e3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 31 Mar 2008 17:56:14 +0000 Subject: [PATCH] Automatic generation of elimination and inversion principles for co-inductive types disabled (since it does not make sense!) --- .../components/library/librarySync.ml | 34 +++++++++++-------- 1 file changed, 19 insertions(+), 15 deletions(-) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index 9c6c53aee..203f78869 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -519,21 +519,25 @@ let add_obj refinement_toolkit uri obj = generate_sibling_mutual_definitions refinement_toolkit uri attrs name bo | Cic.Constant _ -> () - | Cic.InductiveDefinition (_,_,_,attrs) -> - uris := !uris @ - generate_elimination_principles uri refinement_toolkit; - uris := !uris @ generate_inversion refinement_toolkit uri obj; - let rec get_record_attrs = - function - | [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in - (match get_record_attrs attrs with - | None -> () (* not a record *) - | Some fields -> - uris := !uris @ - (generate_projections refinement_toolkit uri fields)) + | Cic.InductiveDefinition (inductivefuns,_,_,attrs) -> + let _,inductive,_,_ = List.hd inductivefuns in + if inductive then + begin + uris := !uris @ + generate_elimination_principles uri refinement_toolkit; + uris := !uris @ generate_inversion refinement_toolkit uri obj; + end ; + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in + (match get_record_attrs attrs with + | None -> () (* not a record *) + | Some fields -> + uris := !uris @ + (generate_projections refinement_toolkit uri fields)) | Cic.CurrentProof _ | Cic.Variable _ -> assert false end; -- 2.39.2