- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof _
- | Intermediate _
- | Proof _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status aliases in
- status, cic
-
-let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
- let interp path = Disambiguate.interpretate_path [] status.aliases path in
- let goal_path = interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let status,wanted =
- match wanted with
- None -> status,None
- | Some wanted ->
- let status,wanted = disambiguate_term status wanted in
- status, Some wanted
- in
- status, (wanted, hyp_paths ,goal_path)
-
-let disambiguate_tactic status = function
- | TacticAst.Apply (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Apply (loc, cic)
- | TacticAst.Absurd (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Absurd (loc, cic)
- | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
- | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
- | TacticAst.Change (loc, pattern, with_what) ->
- let status, with_what = disambiguate_term status with_what in
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Change (loc, pattern, with_what)
- | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
- | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
- | TacticAst.Compare (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Compare (loc,term)
- | TacticAst.Constructor (loc,n) ->
- status, TacticAst.Constructor (loc,n)
- | TacticAst.Contradiction loc ->
- status, TacticAst.Contradiction loc
- | TacticAst.Cut (loc, ident, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Cut (loc, ident, cic)
- | TacticAst.DecideEquality loc ->
- status, TacticAst.DecideEquality loc
- | TacticAst.Decompose (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Decompose(loc,term)
- | TacticAst.Discriminate (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Discriminate(loc,term)
- | TacticAst.Exact (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Exact (loc, cic)
- | TacticAst.Elim (loc, term, Some term') ->
- let status, cic1 = disambiguate_term status term in
- let status, cic2 = disambiguate_term status term' in
- status, TacticAst.Elim (loc, cic1, Some cic2)
- | TacticAst.Elim (loc, term, None) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Elim (loc, cic, None)
- | TacticAst.ElimType (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.ElimType (loc, cic)
- | TacticAst.Exists loc -> status, TacticAst.Exists loc
- | TacticAst.Fail loc -> status,TacticAst.Fail loc
- | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, term = disambiguate_term status term in
- status, TacticAst.Fold (loc,reduction_kind, term, pattern)
- | TacticAst.FwdSimpl (loc, hyp, names) ->
- status, TacticAst.FwdSimpl (loc, hyp, names)
- | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
- | TacticAst.Generalize (loc,pattern,ident) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Generalize(loc,pattern,ident)
- | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
- | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
- | TacticAst.Injection (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Injection (loc,term)
- | TacticAst.Intros (loc, num, names) ->
- status, TacticAst.Intros (loc, num, names)
- | TacticAst.LApply (loc, depth, to_what, what, ident) ->
- let f term (status, to_what) =
- let status, term = disambiguate_term status term in
- status, term :: to_what
- in
- let status, to_what = List.fold_right f to_what (status, []) in
- let status, what = disambiguate_term status what in
- status, TacticAst.LApply (loc, depth, to_what, what, ident)
- | TacticAst.Left loc -> status, TacticAst.Left loc
- | TacticAst.LetIn (loc, term, name) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.LetIn (loc,term,name)
- | TacticAst.Reduce (loc, reduction_kind, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Reduce(loc, reduction_kind, pattern)
- | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
- | TacticAst.Replace (loc, pattern, with_what) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, with_what = disambiguate_term status with_what in
- status, TacticAst.Replace (loc, pattern, with_what)
- | TacticAst.Rewrite (loc, dir, t, pattern) ->
- let status, term = disambiguate_term status t in
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Rewrite (loc, dir, term, pattern)
- | TacticAst.Right loc -> status, TacticAst.Right loc
- | TacticAst.Ring loc -> status, TacticAst.Ring loc
- | TacticAst.Split loc -> status, TacticAst.Split loc
- | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
- | TacticAst.Transitivity (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Transitivity (loc, cic)
-
-let rec disambiguate_tactical status = function
- | TacticAst.Tactic (loc, tactic) ->
- let status, tac = disambiguate_tactic status tactic in
- status, TacticAst.Tactic (loc, tac)
- | TacticAst.Do (loc, num, tactical) ->
- let status, tac = disambiguate_tactical status tactical in
- status, TacticAst.Do (loc, num, tac)
- | TacticAst.Repeat (loc, tactical) ->
- let status, tac = disambiguate_tactical status tactical in
- status, TacticAst.Repeat (loc, tac)
- | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- let status, tacticals = disambiguate_tacticals status tacticals in
- let tacticals = List.rev tacticals in
- status, TacticAst.Seq (loc, tacticals)
- | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- let status, tactical = disambiguate_tactical status tactical in
- let status, tacticals = disambiguate_tacticals status tacticals in
- status, TacticAst.Then (loc, tactical, tacticals)
- | TacticAst.Tries (loc, tacticals) ->
- let status, tacticals = disambiguate_tacticals status tacticals in
- status, TacticAst.Tries (loc, tacticals)
- | TacticAst.Try (loc, tactical) ->
- let status, tactical = disambiguate_tactical status tactical in
- status, TacticAst.Try (loc, tactical)
-
-and disambiguate_tacticals status tacticals =
- let status, tacticals =
- List.fold_left
- (fun (status, tacticals) tactical ->
- let status, tac = disambiguate_tactical status tactical in
- status, tac :: tacticals)
- (status, [])
- tacticals
- in
- let tacticals = List.rev tacticals in
- status, tacticals
-
-let disambiguate_command status = function
- | TacticAst.Default _
- | TacticAst.Alias _
- | TacticAst.Include _ as cmd -> status,cmd
- | TacticAst.Coercion (loc, term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Coercion (loc,term)
- | (TacticAst.Set _ | TacticAst.Qed _ | TacticAst.Drop _ ) as cmd ->
- status, cmd
- | TacticAst.Obj (loc,obj) ->
- let status,obj = disambiguate_obj status obj in
- status, TacticAst.Obj (loc,obj)