X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2FannotationHelper%2FcicAnnotationHinter.ml;h=7cf3cddbb8841b44010e1bfe03bb3afae4662ffe;hb=0148419c577eab74538b8e2564a64e399d8bdd65;hp=c5acdf1241bb5762a4a17fce62e580410d1af990;hpb=26992ee777bcfe3aa4d9dcd5166ff78864c8f623;p=helm.git
diff --git a/helm/annotationHelper/cicAnnotationHinter.ml b/helm/annotationHelper/cicAnnotationHinter.ml
index c5acdf124..7cf3cddbb 100644
--- a/helm/annotationHelper/cicAnnotationHinter.ml
+++ b/helm/annotationHelper/cicAnnotationHinter.ml
@@ -94,7 +94,7 @@ let get_id annterm =
match annterm with
C.ARel (id,_,_)
| C.AVar (id,_)
- | C.AMeta (id,_)
+ | C.AMeta (id,_,_)
| C.ASort (id,_)
| C.AImplicit id
| C.ACast (id,_,_)
@@ -103,7 +103,6 @@ let get_id annterm =
| C.ALetIn (id,_,_,_)
| C.AAppl (id,_)
| C.AConst (id,_,_)
- | C.AAbst (id,_)
| C.AMutInd (id,_,_,_)
| C.AMutConstruct (id,_,_,_,_)
| C.AMutCase (id,_,_,_,_,_,_)
@@ -120,9 +119,21 @@ let create_hint_from_term annotation_window annterm =
| C.AVar (id,_) ->
link_hints annotation_window
[| "relURI???", "" |]
- | C.AMeta (id,_) ->
- link_hints annotation_window
- [| "Number", "" |]
+ | C.AMeta (id,_,subst) ->
+ let res =
+ Array.append
+ [| "Number", "" |]
+ (Array.mapi
+ (fun i s ->
+ match s with
+ None ->
+ "Argument " ^ string_of_int i, "_"
+ | Some t ->
+ "Argument " ^ string_of_int i, ""
+ ) (Array.of_list subst)
+ )
+ in
+ link_hints annotation_window res
| C.ASort (id,_) ->
link_hints annotation_window
[| "Value", "" |]
@@ -173,9 +184,6 @@ let create_hint_from_term annotation_window annterm =
| C.AConst (id,_,_) ->
link_hints annotation_window
[| "Uri???", "" |]
- | C.AAbst (id,_) ->
- link_hints annotation_window
- [| "Uri???", "" |]
| C.AMutInd (id,_,_,_) ->
link_hints annotation_window
[| "Uri???", "" |]
@@ -301,8 +309,9 @@ let create_hint_from_obj annotation_window annobj =
| C.ACurrentProof (id,_,conjs,bo,ty) ->
let boid = get_id bo
and tyid = get_id ty
- and conjsid = List.map (fun (_,te) -> get_id te) conjs in
+ and conjsid = List.map (fun (id,_,_,_) -> id) conjs in
link_hints annotation_window
+(*CSC: never tested since the introduction of the new Metas *)
(Array.append
[| "Name", "" ;
"Ingredients", "" ;
@@ -376,6 +385,9 @@ let create_hints annotation_window ids_to_targets xpath =
match Hashtbl.find ids_to_targets xpath with
Cic.Object annobj -> create_hint_from_obj annotation_window annobj
| Cic.Term annterm -> create_hint_from_term annotation_window annterm
+(*CSC: never tested since the introduction of the new Metas *)
+ | Cic.Hypothesis _
+ | Cic.Conjecture _ -> assert false
with
Not_found -> raise (IdUnknown xpath)
;;