From: Claudio Sacerdoti Coen Date: Wed, 12 Jun 2002 16:09:31 +0000 (+0000) Subject: * Abst removed from the DTD X-Git-Tag: V_0_3_0_debian_8~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2ed5c8ffbe419bdba20236d48f078f9980ed2228;p=helm.git * Abst removed from the DTD * Metas completely changed in the DTD --- 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) ;;