--- /dev/null
+*.cm[iox] gTopLevel.opt
BIN_DIR = /usr/local/bin
REQUIRES = lablgtkmathview helm-cic_textual_parser helm-cic_proof_checking \
- helm-xml gdome_xslt
+ helm-xml gdome_xslt helm-cic_unification
PREDICATES =
OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -pp camlp4o
OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS)
in
aux
;;
+
+let print_inner_types curi ids_to_inner_sorts ids_to_inner_types =
+ let module X = Xml in
+ X.xml_nempty "InnerTypes" ["of",UriManager.string_of_uri curi]
+ (Hashtbl.fold
+ (fun id ty x ->
+ [< x ;
+ X.xml_nempty "TYPE" ["of",id]
+ (print_term curi ids_to_inner_sorts ty)
+ >]
+ ) ids_to_inner_types [<>]
+ )
+;;
;;
let acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- metasenv env t
+ ids_to_inner_types metasenv env t
=
let module T = CicTypeChecker in
let module C = Cic in
let fresh_id' = fresh_id seed ids_to_terms ids_to_father_ids in
- let rec aux father bs tt =
+ let rec aux computeinnertypes father bs tt =
let fresh_id'' = fresh_id' father tt in
- let aux' = aux (Some fresh_id'') in
+ let aux' = aux true (Some fresh_id'') in
(* First of all we compute the inner type and the inner sort *)
(* of the term. They may be useful in what follows. *)
(*CSC: This is a very inefficient way of computing inner types *)
| C.Sort C.Type -> "Type"
| _ -> assert false
in
- let innertype,innersort =
+ let ainnertype,innertype,innersort =
let cicenv = List.map (function (_,ty) -> ty) bs in
let innertype = T.type_of_aux' metasenv cicenv tt in
let innersort = T.type_of_aux' metasenv cicenv innertype in
- innertype, string_of_sort innersort
+ let ainnertype =
+ if computeinnertypes then
+ Some (aux false (Some fresh_id'') bs innertype)
+ else
+ None
+ in
+ ainnertype, innertype, string_of_sort innersort
+ in
+ let add_inner_type id =
+ match ainnertype with
+ None -> ()
+ | Some ainnertype -> Hashtbl.add ids_to_inner_types id ainnertype
in
match tt with
C.Rel n ->
| C.Implicit -> C.AImplicit (fresh_id'')
| C.Cast (v,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
C.ACast (fresh_id'', aux' bs v, aux' bs t)
| C.Prod (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id''
C.AProd (fresh_id'', n, aux' bs s, aux' ((n,s)::bs) t)
| C.Lambda (n,s,t) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ begin
+ let father_is_lambda =
+ match father with
+ None -> false
+ | Some father' ->
+ match Hashtbl.find ids_to_father_ids father' with
+ None -> assert false
+ | Some fatherid ->
+ match Hashtbl.find ids_to_terms fatherid with
+ C.Lambda _ -> true
+ | _ -> false
+ in
+ if not father_is_lambda then
+ add_inner_type fresh_id''
+ end ;
C.ALambda (fresh_id'',n, aux' bs s, aux' ((n,s)::bs) t)
| C.LetIn (n,s,t) ->
(*CSC: Nell'environment debbo poter avere anche dichiarazioni! ;-(
*) assert false
| C.Appl l ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
C.AAppl (fresh_id'', List.map (aux' bs) l)
| C.Const (uri,cn) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
C.AMutConstruct (fresh_id'', uri, cn, tyno, consno)
| C.MutCase (uri, cn, tyno, outty, term, patterns) ->
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
C.AMutCase (fresh_id'', uri, cn, tyno, aux' bs outty,
aux' bs term, List.map (aux' bs) patterns)
| C.Fix (funno, funs) ->
let names = List.map (fun (name,_,ty,_) -> C.Name name,ty) funs in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
C.AFix (fresh_id'', funno,
List.map
(fun (name, indidx, ty, bo) ->
| C.CoFix (funno, funs) ->
let names = List.map (fun (name,ty,_) -> C.Name name,ty) funs in
Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
+ if innersort = "Prop" then
+ add_inner_type fresh_id'' ;
C.ACoFix (fresh_id'', funno,
List.map
(fun (name, ty, bo) ->
) funs
)
in
- aux None env t
+ aux true None env t
;;
let acic_of_cic_env metasenv env t =
let ids_to_terms = Hashtbl.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
+ let ids_to_inner_types = Hashtbl.create 503 in
let seed = ref 0 in
acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
- metasenv env t,
- ids_to_terms, ids_to_father_ids, ids_to_inner_sorts
+ ids_to_inner_types metasenv env t,
+ ids_to_terms, ids_to_father_ids, ids_to_inner_sorts, ids_to_inner_types
;;
exception Found of (Cic.name * Cic.term) list;;
let ids_to_terms = Hashtbl.create 503 in
let ids_to_father_ids = Hashtbl.create 503 in
let ids_to_inner_sorts = Hashtbl.create 503 in
+ let ids_to_inner_types = Hashtbl.create 503 in
let seed = ref 0 in
let acic_term_of_cic_term_env' =
- acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts in
+ acic_of_cic_env' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
+ ids_to_inner_types in
let acic_term_of_cic_term' = acic_term_of_cic_term_env' [] [] in
let aobj =
match obj with
C.ACurrentProof ("mettereaposto",id,aconjectures,abo,aty)
| C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
in
- aobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts
+ aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types
;;
"media-type", "'text/html'" ;
"keys", "'d_c%2CC1%2CG%2CC2%2CL'" ;
"interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
- "naturalLanguage", "'no'" ;
+ "naturalLanguage", "'yes'" ;
"annotations", "'no'" ;
+ "explodeall", "'true()'" ;
"topurl", "'http://phd.cs.unibo.it/helm'" ;
"CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
;;
"interfaceURL", "'http%3A//phd.cs.unibo.it/helm/html/cic/index.html'" ;
"naturalLanguage", "'no'" ;
"annotations", "'no'" ;
+ "explodeall", "'true()'" ;
"topurl", "'http://phd.cs.unibo.it/helm'" ;
"CICURI", "'cic:/Coq/Init/Datatypes/bool_ind.con'" ]
;;
input styles
;;
-let mml_of_cic_object annobj ids_to_inner_sorts =
+let mml_of_cic_object annobj ids_to_inner_sorts ids_to_inner_types =
let xml =
Cic2Xml.print_object
(UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts annobj
in
- let input =
- Xml2Gdome.document_of_xml domImpl xml
- in
+ let xmlinnertypes =
+ Cic2Xml.print_inner_types
+ (UriManager.uri_of_string "cic:/dummy.con") ids_to_inner_sorts
+ ids_to_inner_types
+ in
+ let input = Xml2Gdome.document_of_xml domImpl xml in
+(*CSC: We save the innertypes to disk so that we can retrieve them in the *)
+(*CSC: stylesheet. This DOES NOT work when UWOBO and/or the getter are not *)
+(*CSC: local. *)
+ Xml.pp xmlinnertypes (Some "/public/sacerdot/innertypes") ;
let output = applyStylesheets input mml_styles mml_args in
output
;;
None -> assert false
| Some (metasenv,bo,ty) -> Cic.CurrentProof ("unnamed", metasenv, bo, ty)
in
- let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) =
+ let
+ (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types)
+ =
Cic2acic.acic_object_of_cic_object currentproof
in
- let mml = mml_of_cic_object acic ids_to_inner_sorts in
+ let mml = mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types in
output#load_tree mml ;
current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
;;
let refresh_sequent (proofw : GMathView.math_view) =
- let metasenv =
- match !ProofEngine.proof with
- None -> assert false
- | Some (metasenv,_,_) -> metasenv
- in
- let currentsequent =
- match !ProofEngine.goal with
- None -> assert false
- | Some (_,sequent) -> sequent
- in
- let sequent_gdome = SequentPp.XmlPp.print_sequent metasenv currentsequent in
- let sequent_doc =
- Xml2Gdome.document_of_xml domImpl sequent_gdome
- in
- let sequent_mml =
- applyStylesheets sequent_doc sequent_styles sequent_args
- in
- proofw#load_tree ~dom:sequent_mml
+ match !ProofEngine.goal with
+ None -> proofw#unload
+ | Some (_,currentsequent) ->
+ let metasenv =
+ match !ProofEngine.proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let sequent_gdome =
+ SequentPp.XmlPp.print_sequent metasenv currentsequent
+ in
+ let sequent_doc =
+ Xml2Gdome.document_of_xml domImpl sequent_gdome
+ in
+ let sequent_mml =
+ applyStylesheets sequent_doc sequent_styles sequent_args
+ in
+ proofw#load_tree ~dom:sequent_mml
(*
ignore(domImpl#saveDocumentToFile ~doc:sequent_doc
~name:"/public/sacerdot/guruguru1" ~indent:true ()) ;
*)
;;
-let exact rendering_window () =
+let output_html outputhtml msg =
+ htmlheader_and_content := !htmlheader_and_content ^ msg ;
+ outputhtml#source (!htmlheader_and_content ^ htmlfooter)
+;;
+
+(***********************)
+(* TACTICS *)
+(***********************)
+
+let call_tactic tactic rendering_window () =
+ let proofw = (rendering_window#proofw : GMathView.math_view) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
+ begin
+ try
+ tactic () ;
+ refresh_sequent proofw ;
+ refresh_proof output
+ with
+ e ->
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>") ;
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal ;
+ end
+;;
+
+let call_tactic_with_input tactic rendering_window () =
let proofw = (rendering_window#proofw : GMathView.math_view) in
let output = (rendering_window#output : GMathView.math_view) in
+ let output = (rendering_window#output : GMathView.math_view) in
+ let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
let inputt = (rendering_window#inputt : GEdit.text) in
+ let savedproof = !ProofEngine.proof in
+ let savedgoal = !ProofEngine.goal in
(*CSC: Gran cut&paste da sotto... *)
let inputlen = inputt#length in
let input = inputt#get_chars 0 inputlen ^ "\n" in
in
try
while true do
- (* Execute the actions *)
match
CicTextualParserContext.main context CicTextualLexer.token lexbuf
with
None -> ()
| Some expr ->
- try
- ProofEngine.exact expr ;
- proofw#unload ;
- refresh_proof output
- with
- e ->
- print_endline ("? " ^ CicPp.ppterm expr) ; flush stdout ;
- raise e
+ tactic expr ;
+ refresh_sequent proofw ;
+ refresh_proof output
done
with
CicTextualParser0.Eof ->
inputt#delete_text 0 inputlen
| e ->
- print_endline ("Error: " ^ Printexc.to_string e) ; flush stdout
+prerr_endline ("? " ^ Printexc.to_string e) ; flush stderr ;
+ output_html outputhtml
+ ("<h1 color=\"red\">" ^ Printexc.to_string e ^ "</h1>");
+ ProofEngine.proof := savedproof ;
+ ProofEngine.goal := savedgoal
;;
-let intros rendering_window () =
- let proofw = (rendering_window#proofw : GMathView.math_view) in
- let output = (rendering_window#output : GMathView.math_view) in
- begin
- try
- ProofEngine.intros () ;
- with
- e ->
- print_endline "? Intros " ;
- raise e
- end ;
- refresh_sequent proofw ;
- refresh_proof output
+let intros rendering_window = call_tactic ProofEngine.intros rendering_window;;
+let exact rendering_window =
+ call_tactic_with_input ProofEngine.exact rendering_window
+;;
+let apply rendering_window =
+ call_tactic_with_input ProofEngine.apply rendering_window
;;
+(**********************)
+(* END OF TACTICS *)
+(**********************)
+
exception OpenConjecturesStillThere;;
exception WrongProof;;
begin
(*CSC: Wrong: [] is just plainly wrong *)
let proof = Cic.Definition ("unnamed",bo,ty,[]) in
- let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts) =
+ let
+ (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
+ ids_to_inner_types)
+ =
Cic2acic.acic_object_of_cic_object proof
in
- let mml = mml_of_cic_object acic ids_to_inner_sorts in
+ let mml =
+ mml_of_cic_object acic ids_to_inner_sorts ids_to_inner_types
+ in
(rendering_window#output : GMathView.math_view)#load_tree mml ;
current_cic_infos := Some (ids_to_terms,ids_to_father_ids)
end
| None -> assert false (* "ERROR: No selection!!!" *)
;;
-let output_html outputhtml msg =
- htmlheader_and_content := !htmlheader_and_content ^ msg ;
- outputhtml#source (!htmlheader_and_content ^ htmlfooter)
-;;
-
let state rendering_window () =
let inputt = (rendering_window#inputt : GEdit.text) in
let oldinputt = (rendering_window#oldinputt : GEdit.text) in
let introsb =
GButton.button ~label:"Intros"
~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
+ let applyb =
+ GButton.button ~label:"Apply"
+ ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in
let outputhtml =
GHtml.xmhtml
~source:"<html><body bgColor=\"white\"></body></html>"
ignore(window#event#connect#delete (fun _ -> GMain.Main.quit () ; true )) ;
ignore(stateb#connect#clicked (state self)) ;
ignore(exactb#connect#clicked (exact self)) ;
+ ignore(applyb#connect#clicked (apply self)) ;
ignore(introsb#connect#clicked (intros self)) ;
Logger.log_callback :=
(Logger.log_to_html ~print_and_flush:(output_html outputhtml))
| Some (metasenv,bo,ty) -> metasenv,bo,ty
in
let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
- let bo' =
- let rec aux =
- let module C = Cic in
- function
- C.Rel _ as t -> t
- | C.Var _ as t -> t
- | C.Meta meta' when meta=meta' -> term
- | C.Meta _ as t -> t
- | C.Sort _ as t -> t
- | C.Implicit as t -> t
- | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
- | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
- | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
- | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
- | C.Appl l -> C.Appl (List.map aux l)
- | C.Const _ as t -> t
- | C.Abst _ as t -> t
- | C.MutInd _ as t -> t
- | C.MutConstruct _ as t -> t
- | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
- C.MutCase (sp,cookingsno,i,aux outt, aux t,
- List.map aux pl)
- | C.Fix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
- fl
- in
- C.Fix (i, substitutedfl)
- | C.CoFix (i,fl) ->
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, aux ty, aux bo))
- fl
- in
- C.CoFix (i, substitutedfl)
- in
- aux bo
+ let rec aux =
+ let module C = Cic in
+ function
+ C.Rel _ as t -> t
+ | C.Var _ as t -> t
+ | C.Meta meta' when meta=meta' -> term
+ | C.Meta _ as t -> t
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Const _ as t -> t
+ | C.Abst _ as t -> t
+ | C.MutInd _ as t -> t
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,i,aux outt, aux t,
+ List.map aux pl)
+ | C.Fix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
in
- proof := Some (metasenv',bo',ty)
+ let metasenv'' = List.map (function i,ty -> i,(aux ty)) metasenv' in
+ let bo' = aux bo in
+ proof := Some (metasenv'',bo',ty)
;;
+(* Returns the first meta whose number is above the number of the higher meta. *)
let new_meta () =
let metasenv =
match !proof with
(*CSC: deve sparire! *)
let context = cic_context_of_context context in
if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
- refine_meta metano bo []
+ begin
+ refine_meta metano bo [] ;
+ goal := None
+ end
else
raise (Fail "The type of the provided term is not the one expected.")
;;
+
+(* The term bo must be closed in the current context *)
+let apply term =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let metasenv =
+ match !proof with
+ None -> assert false
+ | Some (metasenv,_,_) -> metasenv
+ in
+ let (metano,context,ty) =
+ match !goal with
+ None -> assert false
+ | Some (metano,(context,ty)) ->
+ assert (ty = List.assoc metano metasenv) ;
+ (* Invariant: context is the actual context of the meta in the proof *)
+ metano,context,ty
+ in
+ (*CSC: deve sparire! *)
+ let ciccontext = cic_context_of_context context in
+ let mgu,mgut = CicUnification.apply metasenv ciccontext term ty in
+ let mgul = Array.to_list mgu in
+ let mgutl = Array.to_list mgut in
+ let applymetas_to_metas =
+ let newmeta = new_meta () in
+ (* WARNING: here we are using the invariant that above the most *)
+ (* recente new_meta() there are no used metas. *)
+ Array.init (List.length mgul) (function i -> newmeta + i) in
+ (* WARNING!!!!!!!!!!!!!!!!!!!!!!!!!!!!! *)
+ (* Here we assume that either a META has been instantiated with *)
+ (* a close term or with itself. *)
+ let uninstantiatedmetas =
+ List.fold_right2
+ (fun bo ty newmetas ->
+ match bo with
+ Cic.Meta i ->
+ let newmeta = applymetas_to_metas.(i) in
+ (*CSC: se ty contiene metas, queste hanno il numero errato!!! *)
+ let ty_with_newmetas =
+ (* Substitues (META n) with (META (applymetas_to_metas.(n))) *)
+ let rec aux =
+ function
+ C.Rel _
+ | C.Var _ as t -> t
+ | C.Meta n -> C.Meta (applymetas_to_metas.(n))
+ | C.Sort _
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
+ | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
+ | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
+ | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
+ | C.Appl l -> C.Appl (List.map aux l)
+ | C.Const _ as t -> t
+ | C.Abst _ -> assert false
+ | C.MutInd _
+ | C.MutConstruct _ as t -> t
+ | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+ C.MutCase (sp,cookingsno,i,aux outt, aux t,
+ List.map aux pl)
+ | C.Fix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux ty, aux bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+ aux ty
+ in
+ (newmeta,ty_with_newmetas)::newmetas
+ | _ -> newmetas
+ ) mgul mgutl []
+ in
+ let mgul' =
+ List.map
+ (function
+ Cic.Meta i -> Cic.Meta (applymetas_to_metas.(i))
+ | _ as t -> t
+ ) mgul in
+ let bo' =
+ if List.length mgul' = 0 then
+ term
+ else
+ Cic.Appl (term::mgul')
+ in
+ refine_meta metano bo' uninstantiatedmetas ;
+ match uninstantiatedmetas with
+ (n,ty)::tl -> goal := Some (n,(context,ty))
+ | [] -> goal := None
+;;
(let final_s,final_env =
(List.fold_right
(fun (b,n,t) (s,env) ->
- let (acic,_,_,ids_to_inner_sorts) =
+ let (acic,_,_,ids_to_inner_sorts,_) =
Cic2acic.acic_of_cic_env metasenv env t
in
[< s ;
X.xml_nempty
(match b with
- ProofEngine.Definition -> "Definition"
- | ProofEngine.Declaration -> "Declaration"
+ ProofEngine.Definition -> "Def"
+ | ProofEngine.Declaration -> "Decl"
) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
(Cic2Xml.print_term
(UriManager.uri_of_string "cic:/dummy.con")
) context ([<>],[])
)
in
- let (acic,_,_,ids_to_inner_sorts) =
+ let (acic,_,_,ids_to_inner_sorts,_) =
Cic2acic.acic_of_cic_env metasenv final_env goal
in
[< final_s ;
projects / helm.git / commitdiff