Generation of auxiliary lemmas for inductive types and records moved

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 0fc5f6ab81552d67b66463e753033082e2962373..8f417485abcc6782748f85a54ef6fbab2224e843 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -633,43 +633,6 @@ let eval_coercion status coercion =
   let status = add_moo_content moo_content status in
   { status with proof_status = No_proof }
 
-let generate_elimination_principles uri status =
-  let status' = ref status in
-  let elim sort =
-    try
-      let uri,obj = CicElim.elim_of ~sort uri 0 in
-      status' := MatitaSync.add_obj uri obj !status'
-    with CicElim.Can_t_eliminate -> ()
-  in
-  try
-    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
-    !status'
-  with exn ->
-    MatitaSync.time_travel ~present:!status' ~past:status;
-    raise exn
-
-let generate_projections uri fields status =
- let projections = CicRecord.projections_of uri fields in
-  List.fold_left
-   (fun status (uri, name, bo) -> 
-     try 
-      let ty, ugraph = 
-        CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
-      let attrs = [`Class `Projection; `Generated] in
-      let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
-       MatitaSync.add_obj uri obj status
-     with
-        CicTypeChecker.TypeCheckerFailure s ->
-         HLog.message 
-          ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force s));
-         status
-      | CicEnvironment.Object_not_found uri ->
-         let depend = UriManager.name_of_uri uri in
-          HLog.message 
-           ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
-         status
-  ) status projections
-
 (* to avoid a long list of recursive functions *)
 let eval_from_moo_ref = ref (fun _ _ _ -> assert false);;
  
@@ -793,7 +756,7 @@ let eval_command opts status cmd =
         command_error "Proof not completed! metasenv is not empty!";
       let name = UriManager.name_of_uri uri in
       let obj = Cic.Constant (name,Some bo,ty,[],[]) in
-      MatitaSync.add_obj uri obj status
+      MatitaSync.add_obj uri obj {status with proof_status = No_proof}
   | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion
   | GrafiteAst.Alias (loc, spec) -> 
      let diff =
@@ -887,30 +850,8 @@ let eval_command opts status cmd =
           command_error (
             "metasenv not empty while giving a definition with body: " ^
             CicMetaSubst.ppmetasenv [] metasenv);
-         let status' = ref status in
-         (try
-           status' := MatitaSync.add_obj uri obj !status';
-           (match obj with
-           | Cic.Constant _ -> ()
-           | Cic.InductiveDefinition (_,_,_,attrs) ->
-               status' := generate_elimination_principles uri !status';
-               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 ->
-                   status' := generate_projections uri fields !status')
-           | Cic.CurrentProof _
-           | Cic.Variable _ -> assert false);
-           !status'
-         with exn ->
-           MatitaSync.time_travel ~present:!status' ~past:status;
-           raise exn)
-
+         MatitaSync.add_obj uri obj {status with proof_status = No_proof}
+ 
 let eval_executable opts status ex =
   match ex with
   | GrafiteAst.Tactical (_, tac, None) -> eval_tactical status tac