The `Record class now records also the name of the fields

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

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index d9297bce5d517c20182a8648c220995597171a08..e5bb82786a3b742989a72746aa05f7971491f44c 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -235,8 +235,8 @@ let generate_elimination_principles uri status =
  List.fold_left (fun status sort -> elim sort status) status
   [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]
 
-let generate_projections uri status =
- let projections = CicRecord.projections_of uri in
+let generate_projections uri fields status =
+ let projections = CicRecord.projections_of uri fields in
   List.fold_left
    (fun status (uri, name, bo) -> 
      try 
@@ -328,12 +328,17 @@ let eval_command status cmd =
         let status = MatitaSync.add_obj uri obj status in
          match obj with
             Cic.Constant _ -> status
-          | Cic.InductiveDefinition (_,_,_,attrs)
-              when List.mem (`Class `Record) attrs ->
+          | Cic.InductiveDefinition (_,_,_,attrs) ->
              let status = generate_elimination_principles uri status in
-              generate_projections uri status
-          | Cic.InductiveDefinition (_,_,_,_) ->
-             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 -> status (* not a record *)
+                | Some fields -> generate_projections uri fields status)
           | Cic.CurrentProof _
           | Cic.Variable _ -> assert false