added automathic aliases for _ind _rec and _rect when generated

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index eb355f2ea43c01a9eba147d8fc15e52f8b92256f..0496076e73b26a9968d1eb59b7f9f3e15c4c6029 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -197,7 +197,23 @@ let eval_command status cmd =
         MatitaSync.add_inductive_def
           ~uri ~types ~params:[] ~leftno ~ugraph status
       in
+      (* aliases for the constructors and types *)
       let aliases = env_of_list (extract_alias types uri) status.aliases in
+      (* aliases for the eliminations principles *)
+      let aliases = 
+        let base = String.sub suri 0 (String.length suri - 4)  in
+        env_of_list
+        (List.fold_left (
+          fun acc suffix -> 
+            if List.exists (
+              fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
+            ) status.objects then
+              let u = base ^ suffix in
+              (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
+            else
+              acc
+        ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
+      in
       let status = {status with proof_status = No_proof } in
       { status with aliases = aliases}
   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->