From a6abe3d3a62c87634b838bb3578dfe5a1c94b9c2 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 31 May 2005 09:40:36 +0000
Subject: [PATCH] added automathic aliases for _ind _rec and _rect when
 generated

---
 helm/matita/matitaEngine.ml | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index eb355f2ea..0496076e7 100644
--- 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) ->
-- 
2.39.2